Features
The main functionalities of STSLib may be grouped in four kinds, as illustrated in the figure below:
•
Formal design of software components
• Specific verification for STS
• Runtime support for STS
• Interfacing with other tools: model-checkers or general provers
• Specific verification for STS
• Runtime support for STS
• Interfacing with other tools: model-checkers or general provers
The
STSLib
Big Picture
The
main concept
is STS,
for Symbolic Transition System, that is a dynamic description coupled
with a data type description. A Labelled Transition System or LTS is an
automaton with simple labels,
states are sometimes called control states in this document. STS add to
LTS full data types, guards and
input/output values. We use also another notation which is the
Configuration Graph (or CFG) which
is a LTS but with a data value associated to each control state. The
goal of this project is to get an
integrated framework/API for hierarchical software components based on
Symbolic Transition Systems.
Currently only a part of these tools and interfaces exist.
The simplest process to work with our STSLib is the following:
1. Defining an atomic component with an STS:
(a) Write a .sts file describing the dynamic part and check it with the parser (DynamicParser).
(b) When it is right generate the .java class skeleton (DynamicJavaGenerator).
(c) Then fill the .java class (or use the ADT facilities) and use the loader to get an internal representation of the STS (DynamicLoader).
2. The ADT facility (only experimental not yet integrated):
(a) Use the interface generation DynamicInterfaceGenerator to generate an initial .adt file with the ADT signature compatible with the dynamic part.
(b) Fill the algebraic description and check it with the adequate parser (DataParser).
(c) Then use the translator to generate a full Java class (DataJavaGenerator).
3. Defining a composite:
(a) Define several atomic STSs then build a composite.
(b) You have to add the connection links.
(c) Use the parser (CompositeParser) and the loader (CompositeLoader).
4. Once the composite is built several activities related to verification may take place:
(a) We may build a configuration graph on search for deadlock, reachability, paths, ...
(b) They are several functions to get an external description of STS and CFG, there is for instance an interface with Graphivz. Technique is known but the tool has not been yet implemented.
5. It is also possible to get a runtime support, a Java library has been implemented as part of the STSLib and it provides an implementation of the rendezvous.
It is then possible to run the composite system and to trace the execution.
Download the short pdf presentation.
Currently only a part of these tools and interfaces exist.
The simplest process to work with our STSLib is the following:
1. Defining an atomic component with an STS:
(a) Write a .sts file describing the dynamic part and check it with the parser (DynamicParser).
(b) When it is right generate the .java class skeleton (DynamicJavaGenerator).
(c) Then fill the .java class (or use the ADT facilities) and use the loader to get an internal representation of the STS (DynamicLoader).
2. The ADT facility (only experimental not yet integrated):
(a) Use the interface generation DynamicInterfaceGenerator to generate an initial .adt file with the ADT signature compatible with the dynamic part.
(b) Fill the algebraic description and check it with the adequate parser (DataParser).
(c) Then use the translator to generate a full Java class (DataJavaGenerator).
3. Defining a composite:
(a) Define several atomic STSs then build a composite.
(b) You have to add the connection links.
(c) Use the parser (CompositeParser) and the loader (CompositeLoader).
4. Once the composite is built several activities related to verification may take place:
(a) We may build a configuration graph on search for deadlock, reachability, paths, ...
(b) They are several functions to get an external description of STS and CFG, there is for instance an interface with Graphivz. Technique is known but the tool has not been yet implemented.
5. It is also possible to get a runtime support, a Java library has been implemented as part of the STSLib and it provides an implementation of the rendezvous.
It is then possible to run the composite system and to trace the execution.
Download the short pdf presentation.