Difference between revisions of "ADVANCE D3.2 Model Checking"
From Event-B
Jump to navigationJump to searchimported>Tommy m (Initial page to be filled.) |
imported>Leuschel |
||
(One intermediate revision by one other user not shown) | |||
Line 1: | Line 1: | ||
− | + | == Overview == | |
{{TODO|Fill this paragraph.}} | {{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.}} | {{TODO|Fill this paragraph.}} | ||
− | + | == Available Documentation == | |
{{TODO|Fill this paragraph.}} | {{TODO|Fill this paragraph.}} | ||
− | + | == 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.