SpecPro is a library that checks a given specification and build artifacts that can help the user in the design process of software or cyber-physical systems.
Currently SpecPro supports a structured language based on the Property Specification Patterns (PSPs) defined in [1][2]. The language also supports numerical constraints that are encoded in Linear Temporal Logic (LTL). An example of accepted input can be found here.
SpecPro is a rework and extension of snl2fl.
SpecPro is open source software released under the LGPLv3 license. If you use it, please acknowledge it by citing:
@inproceedings{narizzano2018consistency,
title={Consistency of property specification patterns with boolean and constrained numerical signals},
author={Narizzano, Massimo and Pulina, Luca and Tacchella, Armando and Vuotto, Simone},
booktitle={NASA Formal Methods Symposium},
pages={383--398},
year={2018},
organization={Springer}
}
You can build a new distribution of the software simply running in the project dir the following command:
./gradlew build
It will automatically build a .zip and a .tar files in the build/distributions
directory.
To run SpecPro simply decompress one of the two files and execute the command
./bin/SpecPro
It will prompt the help message showing the list of available options.
Alternatively, you can run the application directly with gradle, substituting argN
as needed.
./gradlew run -PappArgs="['arg1', 'args2', 'args3']"
There are many way to run SpecPro and they differ for the kind of output generated.
Using one of the following flags, it is possible to target one of three main model checker supported:
-
-n
or--nusmv
(default option) to target NuSMV/NuXMV -
-a
or--alta
to target Aalta -
-p
or--panda
to target Panda
For NuSMV, SpecPro also supports the --noinvar
option: it encodes the inequality invariants directly into the LTLSPEC
instead that as INVAR.
SpecPro currently performs three main tasks:
-
-t
(default) translate the requirement specification into the corresponding satisfiability checking problem -
-c
translate and perform the Consistency Checking of the input requirement specification. In order to use this option, theSPECPRO_NUSMV
environment variable has to be set if NuSMV is the chosen model checker, andSPECPRO_AALTA
if Aalta is the choosen one (Panda is currently not supported). -
-m
to perform the Inconsistency Explanation (or equivalently MUC extraction) of the inconsistent specification.SPECPRO_NUSMV
orSPECPRO_AALTA
has to be set as in the consistency checking task.
An exampple is:
./bin/SpecPro --nusmv -t -i <inputfile> -o <outputfile>
There are two grammars used in SpecPro:
- FLGrammar.g4: defines the formal formulae syntax
- RequirementsGrammar.g4: defines the grammar for patterns
The grammars are built using ANTLR4, you need to download and install it in order to rebuild them. The installation guide is available here.
Once you have installed ANTLR4, all you have to do is:
-
Open a terminal and move to the it.sagelab.it.sagelab.fe.snl2fl root directory
-
Build FLGrammar:
antlr4 -o src/main/java/it/sagelab/fe/ltl/parser -package it.sagelab.fe.ltl.parser FLGrammar.g4
-
Build RequirementsGrammar:
antlr4 -o src/main/java/it/sagelab/fe/snl2fl/parser -package it.sagelab.fe.snl2fl.parser RequirementsGrammar.g4
[1] Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Software Engineering, 1999. Proceedings of the 1999 International Conference on, pp. 411–420. IEEE (1999)