AI meets Formal Methods: Qualitative Reasoning and Action Systems

Photo: cokada

We got our work on combining Qualitative Reasoning Techniques with Action Systems accepted at ICFEM 2009 in Rio.

This year the conference was highly competitive with an acceptance rate below 30 percent. The paper integrates Qualitative Differential Equations into Back's Action System formalism for modeling hybrid systems. The work forms part of the MOGENTES Project and aims at model-based testing of hybrid systems.

To our knowledge this is the first time that Qualitative Differential Equations have been merged into a formal development technique. The results are not limited to Action Systems, but apply also to similar formalisms like e.g. Event-B.

Bernhard K. Aichernig, Harald Brandl, and Willibald Krenn. Qualitative action systems. In Proceedings of ICFEM 2009: 11th International Conference on Formal Engineering Methods, Dec 9-12, 2009, Rio de Janeiro, Lecture Notes in Computer Science. Springer-Verlag, 2009. in press. (PDF)

Paper abstract: An extension to action systems is presented facilitating the modeling of continuous behavior in the discrete domain. The original action system formalism has been developed by Back et al. in order to describe parallel and distributed computations of discrete systems, i.e. systems with discrete state space and discrete control. In order to cope with hybrid systems, i.e. systems with continuous evolution and discrete control, two extensions have been proposed: hybrid action sys- tems and continuous action systems. Both use dierential equations (relations) to describe continuous evolution. Our version of action systems takes an alternative approach by adding a level of abstraction: continuous behavior is modeled by Qualitative Dierential Equations that are the preferred choice when it comes to specifying abstract and possibly non-deterministic requirements of continuous behavior. Because their solutions are transition systems, all evolutions in our qualitative action systems are discrete. Based on hybrid action systems, we develop a new theory of qualitative action systems and discuss how we have applied such models in the context of automated test-case generation for hybrid systems.

TAP 2010, June 28 - July 2, Malaga, Spain

Photo: Pat McDonald

I have been invited to serve on the Program Committee of TAP 2010, the 4th International Conference on Tests & Proofs.

The TAP conference is devoted to the convergence of proofs and tests. It combines ideas from both sides for the advancement of software quality.

Gordon Fraser, a former colleague of mine at TU Graz, is co-chairing the PC with Angelo Gargantini. The conference chairs are Yuri Gurevich, Microsoft Research, USA and Bertrand Meyer, ETH Zuerich, Switzerland.

Last year, we had a paper at TAP 2009 on concolic execution of distributed systems (see my conference papers).

To prove the correctness of a program is to demonstrate, through impeccable mathematical techniques, that it has no bugs; to test a program is to run it with the expectation of discovering bugs. The two techniques seem contradictory: if you have proved your program, it's fruitless to comb it for bugs; and if you are testing it, that is surely a sign that you have given up on any hope to prove its correctness.

Accordingly, proofs and tests have, since the onset of software engineering research, been pursued by distinct communities using rather different techniques and tools.

And yet the development of both approaches leads to the discovery of common issues and to the realization that each may need the other. The emergence of model checking has been one of the first signs that contradiction may yield to complementarity, but in the past few years an increasing number of research efforts have encountered the need for combining proofs and tests, dropping earlier dogmatic views of incompatibility and taking instead the best of what each of these software engineering domains has to offer.

The conference will include a mix of invited and submitted presentation, and a generous allocation of panels and informal discussions. All papers will be published in Springer's LNCS series.