Goal and Contract Specification Language

The GCSL is a text-pattern based specification language with an formal semantics given by a temporal logic. This bridges the gap between natural language requirements and formal requirements and supports thereby the requirement formalization process. A early formalization allows reasoning about a architecture before the components are available.
The GCSL is an extension of the Contract Specification Language (CSL) developed in the SPEEDS project (see www.speeds.eu.com). There are some similarities in the set of the text-pattern but the new semantics also covers architectural aspects which had not been considered with the CSL. These architectural aspects are expressed using OCL (Object Constraint Language: www.omg.org/spec/OCL) expressions because this gives the ability to address the architecture and to specify the "for all" and "exists" quantifiers and sets of elements. From the users point of view this expressions are commonly used in UML/SysML development environments like Rational Rhapsody and therefore we assume that the users are familiar with the OCL syntax.
In DANSE the GCSL is used to describe two different kinds of specifications. The first one are contracts like in classical system engineering plus the ability to address architectural aspects of the overall SoS. These specification consider static and dynamic properties and may be fulfilled or not. The other kind of specification are goals which are similar to optimization targets in the sense that the fulfillment of these properties shall be increased.

Contract
To enable the reuse of a verified component in different integration environments not only behavior of the component have to be specified but also assumptions on the integration environment. A contract combines a assumption to the environment with the guaranteed behavior of the component. One example for a embedded system is that a component promises only to respond to a certain trigger event if the frequency of that trigger is lower than a certain threshold.
One major advantage is that compatibility of components can be checked without technically integration them if their contracts as complete. This supports the identification of integration problems in early development phases even before prototypes are available.
In the domain of SoS the ability to characterize architecture by using quantification for the existents of CSs allows to specify generic contracts for the SoS. In the following example contract we refer to the Fire Stations in a city and the number of hosted Fire Fighting Cars. The SoS consists of a possibly changing number of Fire Stations and Fire Fighting Cars but the contracts is equivalent in each case:

Natural language: "All Fire Stations hosts always at least one Fire Fighting Car"
GCSL language: "always( SoS.itsFireStations->forAll(fstation | fstation.hostedFireFightingCars->size() >= 1) )"

Goal
Goals complement the specification by defining the target functions of the SoS engineer as well as the local goals of the constituent systems. On the one hand the overall SoS purpose in terms of metrics can be described in terms of goals. On the other hand the participating constituent systems expect a certain benefit of the cooperation within a SoS. Both aspects can not completely described using contracts because goals could compete with each other. For example in many case cost and quality can not be optimal in the same setting. A trade off between multiple factors is based on a partial fulfillment of each goal.

Natural language: "Always minimize the totalCost of the SoS"
GCSL language: "always( minimize(totalCost(SoS)) )"

The GCSL allows to specify the details of the cost function directly in the SoS model and therefore the goal can directly build upon that cost function. Those cost functions usually can be parameterized by the set of elements to which the function is applied therefore we add the "SoS" as parameter to the function.


More details can be found in the final (and public) version of the GCSL documentation in deliverable D6.3.3 in the download section.
Home About Technical Approach DANSE Goal and Contract Specification Language