Adaptation of State/Transition-Based Methods for Embedded System Testing

Authors: Abdelaziz Guerrouat, Harald Richter

Abstract:

In this paper test generation methods and appropriate fault models for testing and analysis of embedded systems described as (extended) finite state machines ((E)FSMs) are presented. Compared to simple FSMs, EFSMs specify not only the control flow but also the data flow. Thus, we define a two-level fault model to cover both aspects. The goal of this paper is to reuse well-known FSM-based test generation methods for automation of embedded system testing. These methods have been widely used in testing and validation of protocols and communicating systems. In particular, (E)FSMs-based specification and testing is more advantageous because (E)FSMs support the formal semantic of already standardised formal description techniques (FDTs) despite of their popularity in the design of hardware and software systems.

Keywords: Formal methods, testing and validation, finite state machines, formal description techniques.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1076156

References:

[1] Specification and Description Language SDL-92, ITU-T Recommendation Z.100, 1992.
[2] Information processing systems - Open Systems Interconnection - Estelle: A formal description technique based on an extended state transition model, International Standard ISO 9074, 1989.
[3] R. Buessow, R. Geisler, and M. Klar, "Specifying safety-critical embedded systems with statecharts and Z: A case study", In Proceedings of Fundamental Approaches to Software Engineering (FASE-98), Lisbon, 1998.
[4] M. Mendler, G. Luettgen. Statecharts, "From Visual Syntax to Model- Theoretic Semantics", In K. Bauknecht, W. Brauer, and Th. M├╝ck (editors), Workshop on Integrating Diagrammatic and Formal Specification Techniques (IDFST 2001), pages 615-621, Vienna, 2001.
[5] B. Potter, J. Sinclair, and D. Till, "Introduction to Formal Specification and Z (2nd Edition)", Prentice Hall PTR; 1996.
[6] A. V. Aho et al., "An optimisation technique for protocol conformance test generation based on UIO sequences and Rural Chinese Postman Tours", In S. Aggarwal and K. Sabnani, editors, Protocol Specification, Testing, and Verification, New Jersey, 1988.
[7] S. Fujiwara, et al., "Test selection based on finite state models", IEEE transaction on Software Engineering 17(6): 591-603, 1991.
[8] H. Richter et al., "A Concept For a Reliable, Cost-Effective, Real-Time Local-Area Network for Automobiles", In Proceedings of Joint conference Embedded in Munich and Embedded Systems, Munich, 2004.
[9] O. Henniger, A. Ulrich, and H. König, "Transformation of Estelle modules aiming at test case derivation", Chapmann & Hall, 1995.
[10] H. Fouchal, et al., "Generation of timed automata from Estelle specifications", In International Workshop on the Formal Technique ESTELLE, Evry, France, 1998.
[11] A. Avizienis, J-C. Laprie, and B. Randell, "Fundamental Concepts of Computer System Dependability", IARP/IEEE-RAS Workshop on Robot Dependability: Technological Challenge of Dependable, Robots in Human Environments, 2001.
[12] L. A. Corts, P. Eles, and Z. Peng, "Verification of embedded systems using a petri net based representation", In Proceedings of the 13th international symposium on System synthesis, Madrid, 2000.