Ulka Shrotri
ABSTRACT
Statemate Statecharts is widely used to specify the behaviour of reactive systems. The Statemate model checker that is used to analyse a Statemate statechart specification for properties such as state reachability, nondeterminism and races does not scale up to industry size specifications. In this paper we propose a technique - super step analysis - that uses bounded model checking to scale up analysis and yet proves non-reachability of states. The proposed technique is based on the asynchronous time model of Statemate in which a system interacts with its environment only when in a stable configuration. In a stable configuration the system reacts to external stimuli and starts a chain of steps until it reaches the next stable configuration. Stable means that further steps are not possible without new external stimuli. For practical Statemate systems adopting the asynchronous time model, in order to ensure that the system interacts with the environment at predictable intervals, there exists a finite bound on the number of steps between any two successive stable configurations. This finite bound between two stable configurations can be exploited to prove non-reachability of states using bounded model checking. In this paper we describe an algorithm that: First determines a finite upper bound K on the number of steps between any two consecutive stable configurations for a given Statemate model M. Then transforms M into another Statemate model M' whose set of initial configurations is a superset of the set of reachable stable configurations of M. Finally, uses bounded model checking up to bound K on M' to analyse properties of M. The paper concludes with the presentation of the results of applying this algorithm on an application from the automotive domain.
- Harel, D., and Naamad, A. 1991. The Language of Statemate. I-Logix Inc.Google Scholar
- Harel, D. and Naamad, A. 1996. The STATEMATE semantics of statecharts. ACM Trans. Softw. Eng. Methodol. 5, 4 (Oct.), 293--333. Google ScholarDigital Library
- SAL Language Manual. Available at: http://SAL.csl.sri.com/doc/lanaguge-report. pdfhttp://SAL.csl.sri.com/doc/lanaguge-report.pdfGoogle Scholar
- http://sal.csl.sri.com/Google Scholar
- A. Kulkarni, R. Metta, U. Shrotri, and R. Venkatesh. Scaling up Model-Checking, A Case Study. In Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems. Proceedings of the GM R&D Workshop, Bangalore, India, January 2007. Availabe at http://www.springerlink.com/index/k061l35783425944.pdfGoogle Scholar
- Sheeran, M., Singh, S., and Stalmarck, G. Checking safety properties using induction and a SAT-solver. LNCS, 1954:108, 2000. Google ScholarDigital Library
- De Moura, L., and Ruess, H. Bounded model checking and induction: From refutation to verification. In CAV'03. LNCS 2725. Springer-Verlag, 14--26.Google Scholar
- Pike, L. Real-Time System Verification by k-Induction. Technical Report TM-2005-213751, NASA Langley Research Center, May, 2005. Available at: http://www.cs.indiana.edu/~lepike/pub_pages/reint.htmlGoogle Scholar
- Berry, G., and Gonthier, G. The Esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming. 19(2):87--152, 1992. Google ScholarDigital Library
- Bhaduri, P., and Ramesh, S. Model checking of statechart models: Survey and research directions. http://www.citebase.org/cgi-bin/citations?id=oai:arXiv.org:cs/0407038, 2004Google Scholar
- McMillan, K., L. Symbolic Model Checking. Kluwer Academic Publishers, Norwell, MA, 1993. Google ScholarDigital Library
- Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., and Zhu, Y. Symbolic model checking using SAT procedures instead of BDDs. Design Automation Conference, 1999. ACM, 317--320. Google ScholarDigital Library
- Huth, M. Some current topics in model checking. International Journal on Software Tools for Technology Transfer (STTT), Feb 2007. 25--36. Google ScholarDigital Library
- Jhala, R., and Majumdar, R. Software model checking. ACM Computing Surveys., 41(4):1--54, 2009 Google ScholarDigital Library
- Atiya, D., Cataño, N. and Lüttgen, G. Towards a benchmark for model checkers of asynchronous concurrent systems. Technical Report YCS-2006-399, Department of Computer Science, University of York, England, April 2006.Google Scholar
- Booch, G., Rumbaugh, J., and Jacobson, I. The Unified Modeling Language. User Guide. Addison-Wesley, 1998. Google ScholarDigital Library
Index Terms
- Proving unreachability using bounded model checking
Recommendations
Bounded model checking of high-integrity software
HILT '13: Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technologyModel checking [5] is an automated algorithmic technique for exhaustive verification of systems, described as finite state machines, against temporal logic [9] specifications. It has been used successfully to verify hardware at an industrial scale [6]. ...
STATEMATE: A Working Environment for the Development of Complex Reactive Systems
STATEMATE is a set of tools, with a heavy graphical orientation, intended for the specification, analysis, design, and documentation of large and complex reactive systems. It enables a user to prepare, analyze, and debug diagrammatic, yet precise, ...
Bounded model checking of high-integrity software
HILT '13Model checking [5] is an automated algorithmic technique for exhaustive verification of systems, described as finite state machines, against temporal logic [9] specifications. It has been used successfully to verify hardware at an industrial scale [6]. ...
Comments