| title | keywords | tags | sidebar | permalink | summary | |
|---|---|---|---|---|---|---|
Composite Type |
gal composite |
|
home_sidebar |
cgal.html |
Syntax of Composite in GAL. |
A GAL specification can contain one or more composite type declarations.
Our architecture relies on an abstract contract for formalisms called Instantiable Transition Systems ITS that enables semantic composition of GAL, and inductively of hierarchically nested components.
An ITS is basically a labeled Kripke Structure but they can be instantiated and composed (think Composite DP).
This page presents the concrete syntax of composite GAL, please read this document for a more formal overview of GAL semantics and some of their applications, or my habilitation thesis for a formal but less technical overview.
A composite contains instances that are synchronized using labels. There are no variables in a composite, only instances ; the state of a composite assigns a state to each of the nested instances.
The composite progresses by firing synchronizations that are similar to GAL transitions except they can only contain call statements (no assignments).
This communication model inspired by CCS/CSP and Arnold-Nivat style synchronization vectors offers pure event-based communication over a finite set of labels.
The definition of a system as an assembly of components in a specific configuration allows from the modeling side to reuse parts of the models in different use-cases, and helps analyze and detect problems more easily in smaller sub components.
From the model-checking point of view, decomposition is matched in the symbolic engine by hierarchy in the SDD encoding of the state, and can yield orders of magnitude better performance in favorable cases.
Here is an example of a Composite :
{% include_relative galfiles/sample-9.gal.html %}
This small example instantiates two GAL type declarations Ping and Pong as player one p1 and player two p2. p1 has the ball initially; the initial state of the game (which is the main instance) is thus p1:ball=1; p2:ball=0.
Only one synchronization is defined, it passes the ball from p1 to p2, leading to a state where p1:ball=0; p2:ball=1.
The CTL property stating that p2 always ends up with the ball is thus satisfied.
When using a call callee."a" the callee instance that is targeted must progress to one a successor state reached by firing a transition with label "a".
The overall effect of a synchronization is atomic. If the callee instance cannot fire any transition with the label "a" (i.e. the set of successors by label "a" is the empty set), the whole synchronization is aborted.
The semi-column gives us sequential composition semantics. So calling several labels on the same instance can make it progress by more than one transition. This feature makes the composite type very expressive.
Semantics for interleaving of synchronizations are similar to semantics of Petri nets or GAL.
The purpose of Composite type are two-fold :
- From the modeling point of view : It gives us the essential features of an Architectural Description Language. We can model in separately each of the components i.e. GAL or Composite type, they interact through well defined connectors i.e. the finite set of labels, and we can assemble the parts in various configurations for proper model reuse i.e. by changing main.
Use cases include testing of different configurations (typically slowly scaling up the size), reuse of template models (library of model components), easier translations from languages featuring instantiation (e.g. UML), better structure preservation during a translation, easy introduction of "mock" components to analyze parts of the system more easily, ...
- From the model-checking point of view : It gives us structure in the specification, which is exploited to produce more efficient symbolic state encodings, it helps distinguish parts of the system and favors abstraction and abstract reasoning for compositional model-checking, it helps identify similar behaviors (e.g. as represented by several instances of a given type).
There are many convincing examples showing that decompositions can be good for verification efficiency, the NUPN format used in the MCC@ICATPN is a good example of this.
Next Section : Composite Basic Concepts