You are here

Promela translator

One of the most important and widely known model checkers is SPIN designed over 20 years ago by H.J. Holzmann. It is probably the first system proposing a complete and implemented methodology of automatic verification using model checking. An integral part of the SPIN system is Promela (Process or Protocol Meta Language) used to model distributed systems to be verified. The tool represents states directly, as they are defined in the model, but applying some efficient optimization techniques helps to substantially reduce the computational complexity. Promela specifications are direct inputs to SPIN verification system. To the category of tools based on the indirect state space representation belongs the system Verics. In that group of tools it seems that the most promising are those which use propositional formulas to represent the verified systems. Such tools can directly use effective, existing SAT solvers as a basic support for Bounded Model Checking (BMC). Verics implements BMC but it also proposes so called "on-the-fly" verification based on bisimulation or simulation abstractions.The translation from Promela to Timed Automata with Discrete Data (TADD), which can be used as one of input formalisms of Verics, shall give Verics the power comparable to SPIN with additional possibilities: checking a richer set of formulas (CTL) and dealing with systems containing time constraints.We focus on the translation from the original Promela constructs to the network of TADD making the Promela specifications indirectly acceptable for Verics. In this way it will be possible to compare efficiency of Verics and SPIN using some typical examples. On the other hand, the fact that TADD can be accepted as an input by some other tools makes such translation an interesting work not only for Verics users.Now we are working on Promela time extension. We have made a method of translation and first experimental results for timed protocols written in Promela.As for now Promela translator is designed for translation of Promela code into network of extended time automata. The input is being parsed to check if it consist any unsupported constructions such as for example embeded C code. If such constructions are found the warning is produced and that parts of code are ommited in translation process.Usage:  p2ta+ promela_file [automata_file] promela_file is needed as a first parameter of execution. If second parameter is ommited then result of translation is send to standard output else file with given name is created with result of translation.

Back to top