ADVANCE D3.3 Model Checking: Difference between revisions
imported>Nicolas First draft |
imported>Jens |
||
| Line 3: | Line 3: | ||
= Motivations / Decisions = | = Motivations / Decisions = | ||
''' Parallel Model Checking ''' | |||
''' Partial Order Reduction ''' | |||
''' 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.'' | |||
''' 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.'' | |||
''' 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.'' | |||
''' Physical Units''' | |||
''Physical units work will be completed. First experiments with industrial models from Alstom are encouraging.'' | |||
''' 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 = | = Available Documentation = | ||
Revision as of 07:12, 19 August 2013
Overview
TODO
Motivations / Decisions
Parallel Model Checking
Partial Order Reduction
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.
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.
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.
Physical Units Physical units work will be completed. First experiments with industrial models from Alstom are encouraging.
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
TODO
Planning
TODO
