Industrial deployment of system engineering methods providing high dependability and productivity

 

SAL, Kodkod, and BDDs for Validation of B Models. Lessons and Outlook.

Plagge, Daniel and Leuschel, Michael and Lopatkin, Ilya and Iliasov, Alexei and Romanovsky, Alexander (2009) SAL, Kodkod, and BDDs for Validation of B Models. Lessons and Outlook. In: AFM09 (Automated Formal Methods), 27 June 2009, Grenoble, France. (In Press)

[img]
Preview
PDF - Accepted Version
261Kb

Abstract

PROB is a model checker for high-level B and Event-B models based on constraint-solving. In this paper we investigate alternate approaches for validating high-level B models using alternative techniques and tools based on using BDDs, SAT-solving and SMT-solving. In particular, we examine whether PROB can be complemented or even supplanted by using one of the tools BDDBDDB, Kodkod or SAL.

Item Type:Conference or Workshop Item (Paper)
Subjects:Tool developments > Model checking
Tool developments > Rodin plug-ins
ID Code:133
Deposited By:Mr Ilya Lopatkin
Deposited On:13 Jul 2009 12:09
Last Modified:19 Apr 2010 16:05

Repository Staff Only: item control page

Deploy-Project - All right reserved