Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05) (2009)
Nov. 23, 2009 to Nov. 27, 2009
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2009.16
In this paper we present a technique to model different aspects of the same system with different formalisms, while keeping the various models tightly integrated with one another. In a multi-paradigm approach to modeling, formalisms with different natures are used in combination to describe complementary parts and aspects of the system. This can have a beneficial impact on the modeling activity, as different paradigms can be better suited to describe different aspects of complex systems. While each paradigm provides a different view on the many facets of the system, it is of paramount importance that a coherent comprehensive model emerges from the combination of the various partial descriptions. Our approach leverages the flexibility provided by a bounded satisfiability checker to encode the verification problem of the integrated model in the Boolean satisfiability (SAT) problem; this allows users to carry out formal verification activities both on the whole model and on parts thereof. The effectiveness of the approach is illustrated through the example of a monitoring system.
Metric temporal logic, timed Petri nets, timed automata, discretization, dense time, bounded model checking
M. Rossi, M. Pradella, M. M. Bersani and C. A. Furia, "Integrated Modeling and Verification of Real-Time Systems through Multiple Paradigms," 2009 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2009)(SEFM), Hanoi, 2009, pp. 13-22.