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

From Event-B
Jump to navigationJump to search
imported>Tommy
m (Initial page to be filled.)
 
imported>Leuschel
(One intermediate revision by one other user not shown)
Line 1: Line 1:
=== Overview ===
+
== Overview ==
 
{{TODO|Fill this paragraph.}}
 
{{TODO|Fill this paragraph.}}
  
=== Motivations / Decisions ===
+
* TLA to B conversion, support for TLA+ in ProB (motivation: TLA can deal with real numbers,...; extend reach of the project)
 +
 
 +
* Continuous improvements of constraint solving capabilities of ProB
 +
 
 +
* Work towards full support of Theory Plug-in: Support for external and recursive functions, translator, (work in progress)
 +
 
 +
* Finish conversion to Kodkod, experiments with Kodkod and SMT translators
 +
 
 +
* Maybe: initial work on physical units supprt
 +
 
 +
== Motivations / Decisions ==
 
{{TODO|Fill this paragraph.}}
 
{{TODO|Fill this paragraph.}}
  
=== Available Documentation ===
+
== Available Documentation ==
 
{{TODO|Fill this paragraph.}}
 
{{TODO|Fill this paragraph.}}
  
=== Planning ===
+
== Planning ==
 
{{TODO|Fill this paragraph.}}
 
{{TODO|Fill this paragraph.}}
  

Revision as of 13:56, 14 June 2012

Overview

TODO: Fill this paragraph.

  • TLA to B conversion, support for TLA+ in ProB (motivation: TLA can deal with real numbers,...; extend reach of the project)
  • Continuous improvements of constraint solving capabilities of ProB
  • Work towards full support of Theory Plug-in: Support for external and recursive functions, translator, (work in progress)
  • Finish conversion to Kodkod, experiments with Kodkod and SMT translators
  • Maybe: initial work on physical units supprt

Motivations / Decisions

TODO: Fill this paragraph.

Available Documentation

TODO: Fill this paragraph.

Planning

TODO: Fill this paragraph.

References