Specification
Consistency
Checking
Tool
description
SpecCC
a requirement-consistency maintenance framework
to produce consistent representations. It
is developed by Institute of Software,
Chinese Academy of Sciences.
Libraries
which SpecCC
used include
- Standford Parser: provides Stanford Dependencies
output as well as phrase structure trees
- JPype: allows python programs full access to java class libraries
- G4LTL: a Java library for automatically
generating controllers realizing linear temporal logic (LTL) specifications
Contact
Contact
Rongjie
Yan [yrj(at)ios(.)ac(.)cn] if you have any questions related to
SpecCC.
Tutorial
1. Load a specification
for consistency checking by pressing "Load File" button.
2. Select a type of time abstraction technique.
3. Start the transformation process by pressing "Convert" button.
4. Select an item to adjust the input and output variable classifcation and press the rightarrow or leftarrow.
5. Start consistency checking process by pressing "Checking" button.
6.
Speicfy the type of synthesis
techniques.
7. Choose the type of optimized synthesis methods
8. Report the requirement causing the inconsistency, or show that the specification is consistent.
Downloads
A list of
benchmarks with the transformed LTL formulas.
Executable prototype of SpecCC (tested in Linux).
Source code of
SpecCC.
