fomc
Subproject |
H3 |
Categories |
Model checker / solver for hybrid systems |
Overview |
fomc is a model checker for safety properties of hybrid systems, with main focus on systems with large discrete state spaces. fomc performs symbolic backwards fixpoint model-checking, using LinAIGs to represent state spaces. The tool tightly integrates methods as SMT, quantifier elimination, and flowpipe computation, and uses optimization techniques as "onion"-optimization or compression of state set representations with redundancy removal. |
W. Damm, H. Dierks, S. Disch, W. Hagemann, F. Pigorsch, C. Scholl, U. Waldmann, and B. Wirtz. Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces. Science of Computer Programming, Special Issue on Automated Verification of Critical Systems, 2011. Accepted for publication. W. Damm, S. Disch, H. Hungar, S. Jacobs, J. Pang, F. Pigorsch, C. Scholl, U. Waldmann, and B. Wirtz. Exact state set representations in the verification of linear hybrid systems with large discrete state space. In Kedar S. Namjoshi, Tomohiro Yoneda, Teruo Higashino, and Yoshio Okamura, editors, Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, volume 4762 of Lecture Notes in Computer Science, pages 425-440, 2007. W. Damm, A. Mikschl, J. Oehlerking, E.-R. Olderog, J. Pang, A. Platzer, M. Segelken, and B. Wirtz. Automating verification of cooperation, control, and design in traffic applications. In Cliff Jones, Zhiming Liu, and Jim Woodcock, editors, Formal Methods and Hybrid Real-Time Systems, volume 4700 of LNCS, pages 115-169, 2007. W. Damm, S. Disch, H. Hungar, J. Pang, F. Pigorsch, C. Scholl, U. Waldmann, and B. Wirtz. Automatic verification of hybrid systems with large discrete state space. In Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis, volume 4218 of Lecture Notes in Computer Science, 2006. |
|
Dam, Flap Controller, Trainsystem, Lane Change Assistance System |
|
Download |
Click here for the binary. |
Manual |
Just type ./fomc --help on the command line to see how it can be used. |
Status |
Prototype |