|
Verification, Monitoring and Analysis tools |
|
|
|
An objective of the CONTRACT project was to provide methods and tools to analyse distributed applications formally at both design time and runtime, built upon the combination of the theoretical model, contracting languages, verification techniques and approaches based on model checking and norm driven multi-agent systems.
To reach this objective, the project has designed and developed contract verification, monitoring and analysis mechanisms which can function for the contractual environments defined in the Contract Framework and, more specifically, with the Web Services based environments developed by the project.
There are three types of tools developed by the project:
- Verification tools which build on a existing model checking tool (MCMAS) and adapted algorithms and languages developed by the consortium to prove properties of collections of contracts - checking specifically the types of states which could legally be reach and those which could be reached given certain types of violations. These tools perform off-line verification.
- Monitoring tools which adapt the offline tools to carry out limited on-line monitoring by checking subsets of contracts or contract conditions at runtime to monitor correct execution of the running systems. For this components have been created which receive a system events input stream which can be used to evaluate the state of individual parties and the whole system during execution. These tools perform on-line monitoring.
- Analysis tools which provide simple views of contracts and their status, allowing users to step through contract establishment, termination and execution in the Web services application environment in order to allow developers to trace execution flow and debug contract based systems.
These tools make it possible to check certain system properties such as whether or not particular states can be reached legally or which contracts would need to be violated for a state to be reached, as well as what potential states may be reached should certain contracts be violated by certain parties.
|
Copyright 2006 - 2009, IST Contract Project. All rights reserved.
Powered by Mambo - Free Software released under the GNU/GPL License. |
European Commission Framework 6 IST Project
