[Home]

Tools

I implemented (in C) a BDD-based compiler for a boolean symbolic programming language (namely BSP) based on the ideas in [Tro 95a] as well as a BDD package tailored for such interpreter.

A version of the BSP interpreter driving the CUDD (Colorado University Decision Diagrams) package is being developed.

Case Studies

BSP has been used as a model checker in the following case studies.

Automatic validation (via model chekcing) of a Hydroelectric Power Plant ([PT 96]).

Automatic validation of a telecommunication Tributary Equipment Protection Switcher (Ing. Michele Cecconi, ITALTEL).

Automatic synthesis of controllers for Manufacturing Plants ([Tro 97], [Tro 98]).

Automatic synthesis of controllers for Production Cells.

[Home]