The CLTSA allows to verify system properties containing counting expressions. A system in CLTSA is modelled as a set of interacting finite state machines. CLTSA supports Finite State Process notation (FSP) for concise description of component behaviour. In order to use CLTSA to analyse a system modelled as FSP process, the counting fluents and counting expressions can be defined as follows:
Counting Fluent Syntax cfluent name = <{inc_set},{dec_set},{res_set}> initially int
where name is the counting fluent identification, inc_set (dec_set resp.) is the incremental events set , i.e., those whose occurrence increment (decrement) the fluent by one. And res_set is the reset events set, when one of them takes place the counting fluent value goes back to its initial value.
|
In order to use counting fluents for system analysis, properties with counting expressions (as part of a LTL formula) can be verified. The syntax for the assert and formula is the same provided in LTSA plus the counting expressions that can appear as an operand in the formula:
assert name = ... ( cexpr_1 ) ... ( cexpr_n )...
where each expression is an arithmetic inequation conformed by counting fluents, constants or literal numbers as the following examples:
- cfl == 2
- cfl_1 >= cfl_2
- N + cfl_1 != cfl_2 - cfl_3
- ...
System Analysis
Properties verification
You can perform verification of the properties in the same way as for LTL formulas by selecting them from the Check menu. Due to the arithmetic nature of the counting fluent and their finite state representation, you must provide some limits, specifically the lower (minimum) and upper (maximum) values that they can take during the system execution.
You can perform verification of the properties in the same way as for LTL formulas by selecting them from the Check menu. Due to the arithmetic nature of the counting fluent and their finite state representation, you must provide some limits, specifically the lower (minimum) and upper (maximum) values that they can take during the system execution.
What strict means ?
During the analysis if an strict limit has reached and some increment (decrement) event take place, the counting fluent state remains on the limit value and the analysis goes on. On non-strict limit configuration this scenario leads to a fluent-overflow situation and inconclusive analysis as result. To avoid limits queries, you can set them at the fluent definition using the apply keyword as: cfluent name = ... initially int apply [ low .. up ]
where low and up are literal numbers denoting its minimum and maximum value. And brackets "[" means strict limit and parenthesis "(" non-strict limits.
Like for range's definitions, CLTSA provides a way to declare limits that can be used throughout specification: limit limit_name = [ low .. up ]. |
In case of property violation, you can get the trace as in LTSA plus the fluents, counting fluents and counting expression states at each step of the counterexample trace as depicted bellow.
System Simulation
In order to analyse the state evolution of the fluents, counting fluents and counting expression present in a FSP system specification, the LTSA animator was updated to support fluents information.
The following screenshot show how the fluents information are reported during the simulation