\n| \u201dAny district cannot have more than 1 fire station, except if all districts have at least 1\u201d<\/em><\/p>\n <\/em>SoS.itsDistricts<\/span>\u2192exists(<\/span><\/strong>district | district.containedFireStations<\/span>\u2192size() > 1) implies<\/span><\/strong>
\nSoS.itsDistricts<\/span>\u2192forAll(<\/span><\/strong>district | district.containedFireStations<\/span>\u2192size() \u2265 1)<\/span><\/strong><\/td>\n<\/tr>\n\n| \u201dThe mean city area under fire shall be less than 0.01%\u201d<\/em><\/p>\n <\/em>mean(<\/span>SoS.itsDistricts.fireArea<\/span>\u2192sum()<\/span>)<\/strong>\u2264 0.0001<\/td>\n<\/tr>\n\n| \u201dThe fire fighting cars hosted by a fire station shall be used all simultaneously at least once<\/em>\u00a0in 6 months\u201d<\/em><\/p>\n <\/em>SoS.itsFireStations<\/span>\u2192forAll(<\/span><\/strong>fireStation |
\nWhenever [<\/strong>fireStation.hostedFireFightingCars<\/span>\u2192exists(<\/span><\/strong>ffCar | ffCar.isAtFireStation<\/strong><\/span>)<\/span>] occurs,<\/strong><\/p>\n[<\/strong>fireStation.hostedFireFightingCars<\/span>\u2192forall(<\/span><\/strong>ffCar | ffCar.isAtFireStation = false)<\/span>]\u00a0<\/strong><\/p>\noccurs within [6 months])<\/span><\/strong><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\nThe 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.\u00a0We 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 \u201dtrue\u201d.
\nAs described in [ABL13<\/a>],\u00a0these requirements are translated to the “lower-level B-LTL specification” used by Plasma-Lab.
\nEach behavioral pattern\u00a0is 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.
\nThese 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<\/p>\n\\( \\displaystyle
\n\\phi = \\left\\{
\n\\begin{array}{c}
\nG_{\\le k – 6months}(\\Psi_1({\\tt fireStation_1}) \\implies F_{\\le 6months} \\Psi_2({\\tt fireStation_1}))\\\\
\n\\bigwedge\\\\
\nG_{\\le k – 6months}(\\Psi_1({\\tt fireStation_2}) \\implies F_{\\le 6months} \\Psi_2({\\tt fireStation_2}))\\\\
\n\\bigwedge\\\\
\nG_{\\le k – 6months}(\\Psi_1({\\tt fireStation_3}) \\implies F_{\\le 6months} \\Psi_2({\\tt fireStation_3}))\\\\
\n\\end{array}\\right.
\n\\)\nwhere \\(\\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.<\/p>\n <\/p>\n \n\n\n| Componenent<\/th>\n | \\(\\Psi_1\\)<\/th>\n | \\(\\Psi_2\\)<\/th>\n | \\({\\tt fireStation_2}\\)<\/td>\n | \u00a0\\(\\displaystyle \\begin{array}{l}
\n{\\tt fireFightingCar1.isAtFireStation}\\ \\lor\\\\ {\\tt fireFightingCar2.isAtFireStation}\\ \\lor\\\\ {\\tt fireFightingCar3.isAtFireStation} \\end{array}\\)<\/td>\n | \\(\\displaystyle\\begin{array}{l}
\n\\neg {\\tt fireFightingCar1.isAtFireStation}\\ \\land\\\\ \\neg {\\tt fireFightingCar2.isAtFireStation}\\ \\land\\\\ \\neg {\\tt fireFightingCar3.isAtFireStation}
\n\\end{array} \\)<\/td>\n | \\({\\tt fireStation_2}\\)<\/td>\n | \\(\\displaystyle\\begin{array}{l}
\n{\\tt fireFightingCar4.isAtFireStation}\\ \\lor\\\\ {\\tt fireFightingCar5.isAtFireStation}
\n\\end{array}\\)<\/td>\n | \\(\\displaystyle\\begin{array}{l}
\n\\neg {\\tt fireFightingCar4.isAtFireStation}\\ \\land\\\\ \\neg {\\tt fireFightingCar5.isAtFireStation}
\n\\end{array} \\)<\/td>\n | \\({\\tt fireStation_3}\\)<\/td>\n | \\(\\displaystyle\\begin{array}{l}
\n{\\tt fireFightingCar6.isAtFireStation}\\ \\lor\\\\ {\\tt fireFightingCar7.isAtFireStation}
\n\\end{array} \\)<\/td>\n | \\(\\displaystyle\\begin{array}{l}
\n\\neg {\\tt fireFightingCar6.isAtFireStation}\\ \\land\\\\ \\neg {\\tt fireFightingCar7.isAtFireStation}
\n\\end{array} \\)<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\nThen, the obtained B-LTL formula is used in conjunction with the simulation platform\u00a0DESYRE to assess the probability that these goals is met in the specified time range (the simulation time\u00a0for each run was 4 months). By choosing the Monte Carlo option, Plasma-Lab was able to give us the\u00a0following estimation as a result on a given number of runs:<\/p>\n Prob(mean city area under fire \u2264 0.01%) \u2248 92.3%<\/strong><\/p>\n
\nA-RML models based on the CAE incubator example<\/h3>\nWe have design Adaptive RML models based on this CAE incubator example. The models are available in the following Plasma-Lab project: Adaptive_CAE.plasma<\/strong><\/a>.<\/p>","protected":false},"excerpt":{"rendered":"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\u2026<\/p>\n Continue reading<\/span><\/i><\/a> <\/p>\n","protected":false},"author":232,"featured_media":0,"parent":236,"menu_order":0,"comment_status":"closed","ping_status":"open","template":"","meta":{"footnotes":""},"class_list":["post-704","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/704","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/users\/232"}],"replies":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/comments?post=704"}],"version-history":[{"count":86,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/704\/revisions"}],"predecessor-version":[{"id":1937,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/704\/revisions\/1937"}],"up":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/236"}],"wp:attachment":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/media?parent=704"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}} | | | |
![\"SMC](\"https:\/\/project.inria.fr\/plasma-lab\/files\/2013\/01\/DANSE-300x197.png\" "\\"SMC")
<\/a>