Content deleted Content added
No edit summary |
|||
Line 3:
Besides having an appropriate and efficient way for modeling concurrent and distributed systems, one needs a formal verification approach to ensure their correctness. Rebeca is supported by Rebeca Verifier tool, as a front-end, to translate the codes into existing model-checker languages and thus, be able to verify their properties. Modular verification and abstraction techniques are used to reduce the state space and make it possible to verify complicated reactive systems.
== References ==
* M. Sirjani. Formal Specification and Verification of Concurrent and Reactive Systems, PhD Thesis, Department of Computer Engineering, Sharif University of Technology, December 2004.
* M. Sirjani, A. Movaghar. An Object-Based Model for Agents, in Proceedings of Workshop on Agents for Information Management, Austrian Computer Society, October 2002.
== See also ==
| |||