Integrated Modeling and Verification of Real-Time Systems through Multiple Paradigms

TL;DR

This paper introduces a multi-paradigm modeling technique for complex real-time systems, integrating different formalisms into a coherent model and enabling flexible verification using SAT solvers.

Contribution

It presents a novel method to tightly integrate diverse formal models of a system and verify them using bounded satisfiability checking, enhancing modeling and verification flexibility.

Findings

Effective integration of multiple modeling formalisms demonstrated

Verification can be performed on entire models or specific parts

Application example with a monitoring system validates approach

Abstract

Complex systems typically have many different parts and facets, with different characteristics. 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 an be better suited to describe different aspects of the system. 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. 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 addition, our approach leverages the flexibility provided by a bounded satisfiability checker to encode the verification problem of the integrated model in the propositional 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.