PINS.NET - A .NET-based common interface for formal models

OData support
Molnár Vince
Department of Measurement and Information Systems

This work presents a software component that aims to support the formal verification of safety-critical systems. In case of such systems, proving correct behavior is essential and requires a stronger guarantee than what testing can provide. Formally analyzing the system design in early phases of the develop-ment can facilitate a lower cost and higher reliability. In the design phase, formal models of the pro-posed system behavior are designed and evaluated with precise and often automatic algorithms.

One of the traditional automatic approaches is model checking. The are a number of algorithms for model checking, but many formal modelling languages have been developed as well, which are rarely compatible with all the algorithms. In terms of implementation, a tool developer has to implement po-tentially every combination of algorithm and formalism, which requires a higher effort and carries a higher risk of error. The Linux-based model checker LTSmin solves this problem by defining a com-mon interface between formalisms and algorithms that can separate the two worlds, but carries enough information to also support specialized solutions. This interface is called PINS (Partitioned Next-State Interface), which can be the basis of a common solution shared by many tools.

The Fault Tolerant Systems Research Group of the Budapest University of Technology and Economics develops a modelling and analysis tool called PetriDotNet, which could also profit from using the PINS interface. It is not enough, however, to rewrite the interface in C# (the native language of Petri-DotNet) – the original interface has to be wrapped in order to carry over the already supported model-ling formalisms. The goal of this work is to solve this problem, which proved to be highly nontrivial due to the incompatible technologies of the .NET framework and the Linux operating system.

The final solution managed to combine LTSmin-PINS with a .NET-based wrapper interface in a single process. This – besides enabling PetriDotNet to benefit from the interface – supports the integration of the PINS.NET project in any .NET-based tool. As a secondary result, an object oriented C++ interface has also been created to support Windows-based C++ applications in using the Linux-based interface.

The work is not yet complete, however, as the current code is working, but experimental prototype that should provide the basis for future development. The complicated part – integrating the different tech-nologies – has nevertheless been accomplished.


Please sign in to download the files of this thesis.