Automatic verification of embedded system based on EFSM

Jinjiang Liu, Jingjing Liang

School of Computer and Information Technology, Nanyang Normal University, Nanyang473061, Henan Province, China

To ensure the correctness of embedded system, automation of test case generation is necessary in industrial. This paper present a technique for specifying coverage criteria and a method for generating test suites for embedded systems whose behaviours is depend on its interactive environment. The embedded system under test can be described as extended finite state machines (EFSM) and the coverage criteria can be specified as monitor automata with parameters, which monitor and accept traces that cover a given test criterion of an EFSM. The flexibility of the technique is demonstrated by specifying a number of well-known coverage criteria based on control- and data-flow information using observer automata with parameters. We also develop a method for generating test cases from coverage criteria specified as observers. It is based on transforming a given observer automata into a bitvector analysis problem that can be efficiently implemented as an extension to an existing state-space exploration such as, e.g. SPIN or Uppaal.