Imperial College London released RMCS (Runtime Monitoring of Contracts for Services) v0.2 on 12th January 2009. RMCS utilises a symbolic approach based on bounded model checking and timed automata for the online verification of contracts in a service based environment. Contracts are represented as extended networks of timed automata with constraints specified over integer and boolean variables. They are formally specified using an extended form of the XML format generated by the model checker UPPAAL for real time systems. The extensions included colouring of states as green/red within the model in order to define compliance/violation of contracts respectively. The monitoring engine itself has been derived from the SAT based symbolic model checker Verics. See http://ist-contract.org/index.php?option=com_docman&task=doc_download&gid=29&Itemid=44 for more details.

Several interesting and complex use cases, within and outside the context of the project have been successfully monitored and analysed using RMCS. These include the reference e-shopping case study chosen for the project. Collaboration with use case partner Y'All was specifically undertaken to develop, model and monitor contracts for the various services defined within their case study.