Investigating partial modelling techniques to improve scalability of automated reasoning
As software systems grow larger and more complex, the design and verification of them become extremely difficult. One of the ways to cope with the growing complexity of software development is to allow systems to be only partially modeled. This approach relies on the ability to support several operations on partial models, so that different partially modeled components could be automatically integrated into a single, correctly functioning program. Existing formalisms for partial modeling suffer from the problem that operations on models are complex, and thus can only be applied to small systems.
This activity aims at defining a new formalism, for which manipulations of partial models can be achieved inexpensively without compromising too much on expressive power. A first attempt is to describe must and may behavioural traces as regular expressions (REs). These can be represented as automata, and manipulated in linear time. However, regular expressions are less expressive than other modelling formalisms: for example, they cannot express triggered scenarios. Instead, we are looking to enrich regular expressions with trigger abilities, to identify a “sweet spot: a language with sufficient expressive power and yet with low-complexity analysis for the software-engineering tasks of (1) synthesis of operational models (to check whether requirements are consistent and to help visualize/animate portions of the models for debugging purposes), (2) model-checking with respect to the appropriate temporal logic, (3) refinement of partial models (to facilitate addition of information and reduce under-specification), (4) parallel composition of partial models (so as to put them together into a larger system), and (5) merging of models (so as to compose information coming from multiple sources).
The commonly used formalism to support the partial modeling paradigm is that of Modal Transition Systems (MTSs) [LT88, FBDCU10]. Using MTSs, one can describe traces of behaviours that a system must exhibit, as well as those that may exist in it. MTSs are also capable of expressing triggered scenarios, where a prefix of a behaviour trace may appear, and if it does, some suffix behaviour must be possible. The main drawback of MTSs however, is that the complexity of the operations associated with them is EXPTIME-complete [AHL+09,BKLS09]. This restricts the use of MTSs to only modestly sized programs.
[LT88] Kim Guldstrand Larsen and Bent Thomsen. A modal process logic. In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science (LICS'88), pages 203--210, 1988.
[FBDCU10] D. Fischbein, G. Brunet, N D’Ippolito, M. Chechik, S. Uchitel. Weak Alphabet Merging of Partial Behaviour Models. ACM Transactions on Software Engineering and Methodology (TOSEM), 2010, 49 pages. In press.
[AHL+09] Adam Antonik, Michael Huth, Kim Guldstrand Larsen, Ulrik Nyman, and Andrzej Wasowski. Exptime-complete decision problems for modal and mixed specifications. Electr. Notes Theor. Comput. Sci., 242(1):19--33, 2009.
[BKLS09] Nikola Benes, Jan Kretnsky, Kim Guldstrand Larsen, and Jiri Srba. Checking thorough refinement on modal transition systems is Exptime-complete. In ICTAC, pages 112--126, 2009.