Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-checker

1999 ◽  
Vol 11 (6) ◽  
pp. 637-664 ◽  
Author(s):  
Diego Latella ◽  
Istvan Majzik ◽  
Mieke Massink
Keyword(s):  
Spin Model ◽  
Automatic Verification ◽  
Model Checker ◽  
Spin Model Checker

scholarly journals Towards Automated Verification of P Systems Using Spin

2011 ◽  
Vol 2 (3) ◽  
pp. 1-12 ◽  
Author(s):  
Raluca Lefticaru ◽  
Cristina Tudose ◽  
Florentin Ipate
Keyword(s):  
Natural Language ◽  
Spin Model ◽  
P Systems ◽  
Automated Verification ◽  
P System ◽  
Model Checker ◽  
High Level ◽  
Spin Model Checker

This paper presents an approach to P systems verification using the Spin model checker. The authors have developed a tool which implements the proposed approach and can automatically transform P system specifications from P-Lingua into Promela, the language accepted by the well known model checker Spin. The properties expected for the P system are specified using some patterns, representing high level descriptions of frequently asked questions, formulated in natural language. These properties are automatically translated into LTL specifications for the Promela model and the Spin model checker is run against them. In case a counterexample is received, the Spin trace is decoded and expressed as a P system computation. The tool has been tested on a number of examples and the results obtained are presented in the paper.

Research on Model Checking for SELinux Inter-Process Communication

2013 ◽  
Vol 380-384 ◽  
pp. 3826-3829
Author(s):  
Ning Wang ◽  
Sheng Wen Gong ◽  
Huai Xiao Wang
Keyword(s):  
Operating System ◽  
Spin Model ◽  
Finite State Automaton ◽  
Basic Design ◽  
Model Checker ◽  
Process Communication ◽  
Know How ◽  
Finite State ◽  
Inter Process Communication ◽  
Spin Model Checker

SELinux (Security Enhanced Linux) inherited the basic design of LINUX, and it is a high secure operating system. It is important to know how to make the IPC (Inter-Process Communication) for this kind of multi-task and multi-user system. In this paper, Finite State Automaton is used to verify the security of IPC mechanisms of SELinux. Finally, IPC mechanisms are verified with SPIN model checker.

FORMAL VERIFICATION OF P SYSTEMS USING SPIN

2011 ◽  
Vol 22 (01) ◽  
pp. 133-142 ◽  
Author(s):  
FLORENTIN IPATE ◽  
RALUCA LEFTICARU ◽  
CRISTINA TUDOSE
Keyword(s):  
Theoretical Background ◽  
Spin Model ◽  
P Systems ◽  
Modeling Language ◽  
P System ◽  
Model Checker ◽  
Model Ecosystems ◽  
Complex Models ◽  
System Verification ◽  
Spin Model Checker

This paper presents an approach to P system verification using the Spin model checker. It proposes a P system implementation in PROMELA, the modeling language accepted by SPIN. It also provides the theoretical background for transforming the temporal logic properties expressed for the P system into properties of the executable implementation. Furthermore, a comparison between P systems verification using SPIN and NUSMV is realized. The results obtained show that the PROMELA implementation is more adequate, especially for verifying more complex models, such as P systems that model ecosystems.

Sign in / Sign up

Export Citation Format

Share Document