Modelworks® is a tool that compiles distributed state machines into a machine readable dialect of the process algebra of Communicating Sequential Processes, CSPm. Each state machine takes the form of a precondition that enables an action. The state machines communicate with each other over various pre-defined media that have specified properties such as: being asynchronous or synchronous; being point-to-point or broadcast; being fallible through message loss, or re-ordering, or late delivery etc.
Failures can be injected into the systems represented in Modelworks® to model failures that can arise from faulty components such as when software does not behave as intended. The eventual representation in CSPm has been carefully optimised to be efficient with respect to the process of refinement model checking. Model checking is simply the exploration of a finite set of states1 to determine whether specified properties hold.
Most model checkers are symbolic based on (Ordered) Binary Decision Diagrams (BDD) that can represent large sets of states by, hopefully relatively small logical formulae. The model checking employed by Modelworks® uses explicit-state exploration. This has the advantage that it is not necessary to calculate the entire transition relation in advance; it can be evolved on-the-fly.
Recent advances in the model checker for Modelworks® means that it can exploit parallel cores on modern laptops. This has led to significant performance increases that compare favourably with existing model checkers throughout the world. The performance increase means that system components can be checked at a level of granularity that does not require human intervention to exploit a divide and conquer strategy. Human generated models already break down into subsystems and components; it is just a matter of being able to automatically check these parts and then compose the parts together to produce an overall check of the system.
Modelworks® supports compositional reasoning because it supports refinement checking (where a model of a system satisfies a specification of that system) and because CSPm is inherently compositional. Indeed this approach has been used as part of an induction argument to prove properties of infinite systems. Modelworks® has a front end that semantically translates a Simulink Stateflow model into Modelworks® for analysis. Front ends for SysML and UML will be developed in the near future.
1Note that although the system may have a finite set of states, the system can still exhibit infinite repeated behaviours.
Enter your email address below to obtain a copy of our Modelworks® overview document by return.