Steven P. Miller
Abstract
A translator framework enables the use of model checking in complex avionics systems and other industrial settings.
- Clarke, E., Grumberg, O. and Peled, D. Model Checking. The MIT Press, Cambridge, MA, 2001.Google Scholar
- Esterel Technologies. SCADE Suite Product Description; http://www.estereltechnolgies.com/Google Scholar
- Halbwachs, N., Caspi, P., Raymond, P and Pilaud, D. The synchronous dataflow programming language Lustre. In Proceedings of the IEEE 79, 9 (1991) 1305--1320.Google ScholarCross Ref
- Holzmann, G. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 2003. Google ScholarDigital Library
- IRST. The NuSMV Model Checker; http://nusmv.irst.itc.it/Google Scholar
- The Mathworks Simulink Product Description; http://www.mathworks.com/Google Scholar
- Miller, S., Anderson, E., Wagner, L., Whalen, M. and Heimdahl, M.P.E. Formal verification of flight critical software. In Proceedings of the AIAA Guidance, Navigation and Control Conference and Exhibit (San Francisco, CA, Aug. 15--18, 2005).Google ScholarCross Ref
- Miller, S., Tribble, A., Whalen, M. and Heimdahl, M.P.E. Proving the Shalls. International Journal on Software Tools for Technology Transfer (Feb. 2006).Google Scholar
- Prover Technology. Prover Plug-In Product Description; http://www.prover.com/Google Scholar
- Reactive Systems, Inc.; http://www.reactive-systems.com/Google Scholar
- SRI International. Symbolic Analysis Laboratory; http://sal.csl.sri.com/Google Scholar
- Whalen, M., Cofer, D., Miller, S. Krogh, B., and Storm, W. Integration of formal analysis into a model-based software development process. In Proceedings of the 12th International Workshop on Formal Methods for Industrial Critical Systems (Berlin, Germany, July 1--2, 2007). Google ScholarDigital Library
- Whalen, M., Innis, J., Miller, S. and Wagner, L. ADGS-2100 Adaptive Display & Guidance System Window Manager Analysis. NASA Contractor Report CR-2006--213952 (Feb. 2006); http://shemesh.larc.nasa.gov/fm/fm-collins-pubs.html/Google Scholar
Index Terms
- Software model checking takes off
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]. ...
Accelerating counterexample detection in software model checking
ICSE '18: Proceedings of the 40th International Conference on Software Engineering: Companion ProceeedingsModel checking is an automatic approach in enhancing correctness of systems. However, when it is applied to discover flaws in software systems, most of the respective verification tools lack scalability due to the state-space explosion problem. ...
Reviews
Osman Balci
A commonly used dictum in software testing indicates that "the only exhaustive means of testing is testing until the tester is exhausted!" Not so, say the authors of this paper, if your software is implementing a model representing some logic that lends itself to formal mathematical verification. Miller, Whalen, and Cofer present a translator framework to enable the use of model checkers to determine if a model satisfies a given set of properties. A model checker is created to consider all possible combinations of inputs and state, thus enabling exhaustive testing of the model. After a small example, the authors present an overview of three case studies in which they have applied their tools for model checking. The first one deals with a commercial aircraft's adaptive display and guidance system window manager. The other two deal with the operational flight program of an unmanned aerial vehicle. The case studies conclude that model checking can be effectively used to discover errors early in the development life cycle, for many classes of models. This is an interesting paper. I recommend it to software testing researchers, practitioners, and managers. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments