Jocelyn Simmonds


Runtime Monitoring and Recovery

This project builds on our Runtime Monitoring framework. When the violations are discovered at runtime, we automatically propose and rank recovery plans which users can then select for execution. For some of the violations, such plans essentially involve ``going back'' -- compensating the occurred actions until an alternative behaviour of the application is possible. For other violations, such plans include both ``going back'' and ``re-planning'' -- guiding the application towards a desired behaviour.

Status: submitted for publication. We are in the process of evaluating our framework.

Runtime Monitoring

For a system of distributed processes, correctness can be ensured by (statically) checking whether their composition satisfies properties of interest. In contrast, web services are being designed so that each partner discovers properties of others dynamically, through a published interface. Since the overall system may not be available statically and since each business process is supposed to be relatively simple, we propose to use runtime monitoring of conversations between partners as means of checking behavioural correctness of the entire web service system. Specifically, we identify a subset of UML 2.0 Sequence Diagrams as a property specification language and show that it is sufficiently expressive for capturing safety and liveness properties. By transforming these diagrams to automata, we enable conformance checking of finite execution traces against the specification.

Status: see RV '08, IEEE TSC '09 papers.


XChek is a multi-valued symbolic model checker. It is a generalization of an existing symbolic model checking algorithm to an algorithm for amulti-valued extension of CTL (XCTL). Given a system and a XCTL property, XChek returns the degree to which the system satisfies the property.

The main features of Chek are the following:
+ Multi-valued logics: 2-valued, 3-valued, upset, 4-valued disagreements, etc. Users can define their own logics.
+ Multiple model formats: reads SMV and GCLang models. Multi-valued models are specified in XML.
+ Proof-like counterexamples: proof rules are used to generate counterexamples. Counterexamples can be generated statically or dynamically, and various viewers are available.

Website: XChek and user manual.


VaqTree is a tool that efficiently exploits the resolution proof produced by a successful run of BMC to detect vacuity of LTL properties. The goal of this tool is to detect a significant amount of vacuity when compared to the naive method, with faster runtimes. Results presented at FMCAD '07.

Website: VaqTree, test data and results.

Older projects are available on my previous website at the Universidad de Chile.