Vereofy
Encyclopedia
Vereofy is a software model checker for component-based systems for operational correctness. It was written by Prof. Christel Baier at Technische Universität Dresden. Vereofy uses constraint automata
as formal semantics for the components behavior and for Reo Coordination Language
. Vereofy allows for linear and branching time model checking. The model checker can be used as a stand-alone tool or via an Eclipse (software)
plug-in.
and Constraint Automata Reactive Module Language. They are equally powerful and rely on the same semantic model.
Constraint automata
In computer science, Constraint automata are a formalism to describe the behavior and possible data flow in coordination models. It was introduced by Arbab et al...
as formal semantics for the components behavior and for Reo Coordination Language
Reo Coordination Language
In computer science, Reo is a channel-based exogenous coordination language.- Overview :In the context of distributed application, correction and validity of single processes does not imply the correctness of the whole system. In such systems, the communication between the processes is of a high...
. Vereofy allows for linear and branching time model checking. The model checker can be used as a stand-alone tool or via an Eclipse (software)
Eclipse (software)
Eclipse is a multi-language software development environment comprising an integrated development environment and an extensible plug-in system...
plug-in.
Input Languages
Vereofy uses two input languages: Reo Coordination LanguageReo Coordination Language
In computer science, Reo is a channel-based exogenous coordination language.- Overview :In the context of distributed application, correction and validity of single processes does not imply the correctness of the whole system. In such systems, the communication between the processes is of a high...
and Constraint Automata Reactive Module Language. They are equally powerful and rely on the same semantic model.