Systems of Systems

Important!

All the technical details about the contract language are in this techinal report. It gives all the details about the SMC process for Systems of Systems and the full specification of the Goal Specification Contract Language.

Recently, in DANSE [ABL13], we adapt the SMC techniques to treat large heterogeneous systems like Systems of Systems. Among them, one finds systems integrating multiple heterogeneous distributed applications communicating over a shared network. We proposed to extend UPDM specification – the SoS specification – with some requirements that the SoS must satisfy. These requirements, are specified with the contract language we specially designed for the SoS’s. This language is a combination of the Object Constraint Language (OCL) and the contract patterns of the CSL à la ”SPEEDS”. The SPEEDS contract specification patterns are used to give a high-level specification of real-time components. They have been introduced to enable the user to reason about event triggering that are equivalently replaced in DANSE by property satisfaction. The properties handled by these patterns are about the state of a SoS. We use OCL to specify these state properties. This language allows to build some behavioral properties to express some temporal relations about facts or events of the system denoted by the state properties. It is sufficiently powerful to describe precisely a state of a SoS. These requirements are viewed as behavioral objectives that support the SoS architect in assessing different strategies and finding the best ones. As shown in the following figure, these contracts are compiled into B-LTL formulas that are verified against the SoS (whose constituent systems are compiled into FMI executables) using Plasma-Lab combined with the efficient simulation engine DESYRE developed by Ales. The SMC tool-chain gives an estimation of the satisfiability of the contract by the SoS. The different results help the SoS architect to make good decisions about how to optimize the SoS strategies.

Overview of the DANSE SMC process

Illustration using the CAE incubator

In the frame of the DANSE project, the Concept Alignment Example (CAE) is a fictive SoS example inspired by real-world Emergency Response data to a city fire. It has been built as a playground to demonstrate new methods and models for the analysis and visualization of SoS designs. All structural modeling has been performed using UPDM views, and behaviors have been added on a subset of the constituents that we called ”CAE incubator”, using simple SysML constructs (modeled in state machines) extended by a few stereotypes (e.g. for storing stochastic information). Behavioral modeling in the CAE incubator is focused on following constituent systems: Fire HQ, Fire Station, Fire Fighting Car and District. The city districts have been added as constituent systems because they play an important role in the SoS: their behavior describes how the fires arise, expand and spread to neighbor districts. In the frame of the CAE, all behaviors are abstracted in state machines using IBM Rhapsody, but it would be possible to use any other language and tool as long as it is compliant with the FMI export format. The following figure shows the overall architecture of the CAE incubator as well as the behavior of one of the constituent types: a fire fighting car. We attached to the CAE incubator the following requirements, written accordingly to our proposed
formalism:

”Any district cannot have more than 1 fire station, except if all districts have at least 1”

SoS.itsDistricts→exists(district | district.containedFireStations→size() > 1) implies
SoS.itsDistricts→forAll(district | district.containedFireStations→size() ≥ 1)

”The mean city area under fire shall be less than 0.01%”

mean(SoS.itsDistricts.fireArea→sum())≤ 0.0001

”The fire fighting cars hosted by a fire station shall be used all simultaneously at least once in 6 months”

SoS.itsFireStations→forAll(fireStation |
Whenever [fireStation.hostedFireFightingCars→exists(ffCar | ffCar.isAtFireStation)] occurs,

[fireStation.hostedFireFightingCars→forall(ffCar | ffCar.isAtFireStation = false)]

occurs within [6 months])

The previous table illustrates the kind of properties that we express with a new contract language we developed for extending the SysML/UPDM specifications of SoS. We use syntactic coloring to distinguish the different parts of the language used in the property: the words in red are identifiers from the model, the blue part is from OCL and bold black keywords are temporal operators. These requirements show the capabilities of our language using different requirements of this use case. Whereas the requirement 1 is purely structural, the requirements 2 and 3 are relative to the execution of the SoS: the first one is written using strictly OCL, the second one shows the cumulative operators we introduced and the third one is defined with a behavioral pattern. The presented requirements are contracts without assumption or, more precisely, they are contracts with an assumption that is implicitly ”true”.
As described in [ABL13], these requirements are translated to the “lower-level B-LTL specification” used by Plasma-Lab.
Each behavioral pattern is translated in a equivalent B-LTL scheme combined with the state propositions expressed in OCL. Thus, a formula can starts with quantification expressed with OCL.
These quantification opertors are defined over the initial state of the SoS, and there are compiled in order to simplify the job of the B-LTL checker in Plasma-Lab. As example, we breifly present the translation of the requirement 3. In order to achieve this translation, we need the time bound $k = 6\ months$ that we expect for the SoS simulation. We obtain a formula

$\displaystyle \phi = \left\{ \begin{array}{c} G_{\le k - 6months}(\Psi_1({\tt fireStation_1}) \implies F_{\le 6months} \Psi_2({\tt fireStation_1}))\\ \bigwedge\\ G_{\le k - 6months}(\Psi_1({\tt fireStation_2}) \implies F_{\le 6months} \Psi_2({\tt fireStation_2}))\\ \bigwedge\\ G_{\le k - 6months}(\Psi_1({\tt fireStation_3}) \implies F_{\le 6months} \Psi_2({\tt fireStation_3}))\\ \end{array}\right.$

where $\Psi_1({\tt fireStation_i})$ and $\Psi_2({\tt fireStation_i})$ correspond to the OCL expressions in brackets, e.g. ${\tt fireStation.hostedFireFightingCars\rightarrow exists(isAtFireStation)}$ and ${\tt fireStation.hosted-}$ ${\tt FireFightingCars\rightarrow forall(isAtFireStation = false)}$ . For the OCL quantification operators, we unfold the OCL quantifications that occur in $\Psi_1$ and $\Psi_2$ . The next table gives the result of this unfolding in $\Psi_1({\tt fireStation_i})$ and $\Psi_2({\tt fireStation_i})$ for each ${\tt fireStation}$ . Finally, replacing all occurences of $\Psi_1({\tt fireStation_i})$ and $\Psi_2({\tt fireStation_i})$ in $\phi$ gives the complete translation in B-LTL.

Componenent	$\Psi_1$	$\Psi_2$	${\tt fireStation_2}$	$\displaystyle \begin{array}{l} {\tt fireFightingCar1.isAtFireStation}\ \lor\\ {\tt fireFightingCar2.isAtFireStation}\ \lor\\ {\tt fireFightingCar3.isAtFireStation} \end{array}$	$\displaystyle\begin{array}{l} \neg {\tt fireFightingCar1.isAtFireStation}\ \land\\ \neg {\tt fireFightingCar2.isAtFireStation}\ \land\\ \neg {\tt fireFightingCar3.isAtFireStation} \end{array}$	${\tt fireStation_2}$	$\displaystyle\begin{array}{l} {\tt fireFightingCar4.isAtFireStation}\ \lor\\ {\tt fireFightingCar5.isAtFireStation} \end{array}$	$\displaystyle\begin{array}{l} \neg {\tt fireFightingCar4.isAtFireStation}\ \land\\ \neg {\tt fireFightingCar5.isAtFireStation} \end{array}$	${\tt fireStation_3}$	$\displaystyle\begin{array}{l} {\tt fireFightingCar6.isAtFireStation}\ \lor\\ {\tt fireFightingCar7.isAtFireStation} \end{array}$	$\displaystyle\begin{array}{l} \neg {\tt fireFightingCar6.isAtFireStation}\ \land\\ \neg {\tt fireFightingCar7.isAtFireStation} \end{array}$

Then, the obtained B-LTL formula is used in conjunction with the simulation platform DESYRE to assess the probability that these goals is met in the specified time range (the simulation time for each run was 4 months). By choosing the Monte Carlo option, Plasma-Lab was able to give us the following estimation as a result on a given number of runs:

Prob(mean city area under fire ≤ 0.01%) ≈ 92.3%

A-RML models based on the CAE incubator example

We have design Adaptive RML models based on this CAE incubator example. The models are available in the following Plasma-Lab project: Adaptive_CAE.plasma.

Illustration using the CAE incubator

A-RML models based on the CAE incubator example

Sponsors