Difference between revisions of "ADVANCE D3.3 Model Checking"

From Event-B
Jump to navigationJump to search
imported>Jens
imported>Jens
Line 7: Line 7:
 
We have developed a version of ProB that is able to verify invariants and assertions and check for deadlocks in parallel on a multicore processor. The restrictions of the execution environment( i.e., Sicstus Prolog does not support multithreading) led to a distributed version of ProB where multiple instances of ProB are spawned and coordinated via sockets. Initial experiments indicate that the approach scales very well if the model is suited for parallel model checking, i.e., it is non-deterministic. The additional overhead of our implementation is at least an order of magnitude lower than the runtime of the model checker. Even if the model is not suited at all, the effect of running the parallel version can be neglected.  
 
We have developed a version of ProB that is able to verify invariants and assertions and check for deadlocks in parallel on a multicore processor. The restrictions of the execution environment( i.e., Sicstus Prolog does not support multithreading) led to a distributed version of ProB where multiple instances of ProB are spawned and coordinated via sockets. Initial experiments indicate that the approach scales very well if the model is suited for parallel model checking, i.e., it is non-deterministic. The additional overhead of our implementation is at least an order of magnitude lower than the runtime of the model checker. Even if the model is not suited at all, the effect of running the parallel version can be neglected.  
  
'''Secondary toolchain'''
+
{{TODO}}'''Secondary toolchain'''
 
   
 
   
  
Line 24: Line 24:
 
Error traces (e.g. leading to deadlocks or invariant violations) detected by TLC are translated back to B and can be verified by ProB.
 
Error traces (e.g. leading to deadlocks or invariant violations) detected by TLC are translated back to B and can be verified by ProB.
  
''' Kodkod'''  
+
{{TODO}} ''' Kodkod'''  
 
''Currently the translation to Kodkod is only applied to axioms when trying to find values for the constants and during the constraint based deadlock check. We plan to restructure ProB's internal programming interfaces in a way that allows to apply Kodkod more easily and make it available for other checks (e.g. constraint-based invariant check, assertion checks).
 
''Currently the translation to Kodkod is only applied to axioms when trying to find values for the constants and during the constraint based deadlock check. We plan to restructure ProB's internal programming interfaces in a way that allows to apply Kodkod more easily and make it available for other checks (e.g. constraint-based invariant check, assertion checks).
 
We will evaluate how we can employ more SMT based techniques in ProB.''
 
We will evaluate how we can employ more SMT based techniques in ProB.''
  
'''  Constraint Solver Improvements '''  
+
{{TODO}}'''  Constraint Solver Improvements '''  
 
''During the further development of ProB's constraint solving it became apparent that it would be helpful to represent the cardinality of a set by a CLP(FD) variable. We plan to change ProB's internal representation of sets in a way that its cardinality can be accessed in this way.
 
''During the further development of ProB's constraint solving it became apparent that it would be helpful to represent the cardinality of a set by a CLP(FD) variable. We plan to change ProB's internal representation of sets in a way that its cardinality can be accessed in this way.
 
To allow a translation from ProB to Kodkod, we implemented an integer interval analysis. We plan to adapt the analysis to set up sizes of deferred sets. This is necessary because ProB chooses a fixed size for a deferred set and sometimes a model has only solutions for a certain size. Currently a user must supply a size manually.''
 
To allow a translation from ProB to Kodkod, we implemented an integer interval analysis. We plan to adapt the analysis to set up sizes of deferred sets. This is necessary because ProB chooses a fixed size for a deferred set and sometimes a model has only solutions for a certain size. Currently a user must supply a size manually.''
  
'''Theory Plugin support'''
+
{{TODO}}'''Theory Plugin support'''
  
  
'''  LTL Fairness'''  
+
{{TODO}}'''  LTL Fairness'''  
 
''Fairness properties are very common when specifying LTL formula. Fairness can be encoded by using standard LTL, but it makes the formula significantly larger. The complexity of the model checking algorithm grows exponentially with the number of used LTL operators in a formula. We plan to incorporate support for fairness directly into the model checker which should lead to a drastic improvement in performance when fairness is used. Additionally, the usability of the model checker is improved by having the ability to specify fairness conditions seperatly from the rest of the LTL formula.''
 
''Fairness properties are very common when specifying LTL formula. Fairness can be encoded by using standard LTL, but it makes the formula significantly larger. The complexity of the model checking algorithm grows exponentially with the number of used LTL operators in a formula. We plan to incorporate support for fairness directly into the model checker which should lead to a drastic improvement in performance when fairness is used. Additionally, the usability of the model checker is improved by having the ability to specify fairness conditions seperatly from the rest of the LTL formula.''
  
Line 44: Line 44:
 
The work on physical unit support has been completed and is available as an optional plug-in available from the ProB update site.
 
The work on physical unit support has been completed and is available as an optional plug-in available from the ProB update site.
  
'''  BMotion Studio '''  
+
{{TODO}}'''  BMotion Studio '''  
 
''We will provide a way to link up other Java-based simulation tools with BMotion Studio. Furthermore, beside working on identified bugs and and rectifying usability issues, we want to create more visual elements to aid humans understand large-scale simulations.''
 
''We will provide a way to link up other Java-based simulation tools with BMotion Studio. Furthermore, beside working on identified bugs and and rectifying usability issues, we want to create more visual elements to aid humans understand large-scale simulations.''
  

Revision as of 13:20, 19 August 2013

Overview

TODO

Motivations / Decisions

Distributed Model Checking

We have developed a version of ProB that is able to verify invariants and assertions and check for deadlocks in parallel on a multicore processor. The restrictions of the execution environment( i.e., Sicstus Prolog does not support multithreading) led to a distributed version of ProB where multiple instances of ProB are spawned and coordinated via sockets. Initial experiments indicate that the approach scales very well if the model is suited for parallel model checking, i.e., it is non-deterministic. The additional overhead of our implementation is at least an order of magnitude lower than the runtime of the model checker. Even if the model is not suited at all, the effect of running the parallel version can be neglected.

TODOSecondary toolchain


Partial Order Reduction

With the increasing number of independency between events in an Event-B model the number of states increases exponentially (The State-Space Explosion Problem). To handle the State-Space Explosion problem a partial order reduction method has been implemented for the ProB Model Checker using the Ample-Sets theory[1]. The implementation reduces the state space by using the events relations of the particular model computed by the Enabling Analysis[2], which is called a single time prior to the Model Checking phase every time the Model Checker is started with the enabled POR preference. The implementation is suited for deadlock and invariant checking. Initial experiments have shown that an effective state space reduction could be achieved if the particular Event-B machine has a high number of independent events as well as high number of invariant preserving events. We plan to extend the partial order reduction method in ProB for the LTL Model Checker.

Partial Guard Evaluation

Another possibility of optimizing the Model Checker for large state space specifications is using the results of the Enabling Analysis in order to save the computation of the guards of events known to be enabled or disabled in some states in the state space. Testing of the guard of an event h can be skipped if the previously executed event g generating the current state disables or enables h. In the first case the computation of the event will be skipped, in the latter only the substitutions of h will be computed. Initial experiments have shown a significant improvement of the performance for a CAN bus case study.

B to TLA+

We developed a transcompiler from B to TLA+ (Temporal Logic of Actions) to verify B specifications with TLC. TLC is an explicit state model checker for TLA+ with an efficient disk-based algorithm and support for temporal formulas and fairness.Our translator is full automatic and supports a large subset of B. Moreover it uses static analyses to verify the correctness of the B specification (e.g. type checking and scope checking) and creates an optimized translation for the validation with TLC. Error traces (e.g. leading to deadlocks or invariant violations) detected by TLC are translated back to B and can be verified by ProB.

TODO Kodkod Currently the translation to Kodkod is only applied to axioms when trying to find values for the constants and during the constraint based deadlock check. We plan to restructure ProB's internal programming interfaces in a way that allows to apply Kodkod more easily and make it available for other checks (e.g. constraint-based invariant check, assertion checks). We will evaluate how we can employ more SMT based techniques in ProB.

TODO Constraint Solver Improvements During the further development of ProB's constraint solving it became apparent that it would be helpful to represent the cardinality of a set by a CLP(FD) variable. We plan to change ProB's internal representation of sets in a way that its cardinality can be accessed in this way. To allow a translation from ProB to Kodkod, we implemented an integer interval analysis. We plan to adapt the analysis to set up sizes of deferred sets. This is necessary because ProB chooses a fixed size for a deferred set and sometimes a model has only solutions for a certain size. Currently a user must supply a size manually.

TODOTheory Plugin support


TODO LTL Fairness Fairness properties are very common when specifying LTL formula. Fairness can be encoded by using standard LTL, but it makes the formula significantly larger. The complexity of the model checking algorithm grows exponentially with the number of used LTL operators in a formula. We plan to incorporate support for fairness directly into the model checker which should lead to a drastic improvement in performance when fairness is used. Additionally, the usability of the model checker is improved by having the ability to specify fairness conditions seperatly from the rest of the LTL formula.

It is already possible to use fairness by using the B to TLA translator and run TLC.

Physical Units

The work on physical unit support has been completed and is available as an optional plug-in available from the ProB update site.

TODO BMotion Studio We will provide a way to link up other Java-based simulation tools with BMotion Studio. Furthermore, beside working on identified bugs and and rectifying usability issues, we want to create more visual elements to aid humans understand large-scale simulations.

Available Documentation

Distributed Model Checking

An extended abstract has been published at the Rodin User and Developer Workshop 2013[3].

Planning

TODO

References

  1. Baier,Katoen: Principles of Model Checking, MIT Press, 2008
  2. Bendisposto, Leuschel: Automatic Flow Analysis for Event-B, Proceedings of FASE, 2011, LNCS, Springer
  3. http://tucs.fi/publications/view/?pub_id=pBuHaWa13a