Formal Safety and Security Assessment of an Avionic Architecture with Alloy

abstract sig Port{status: Status,value: Value} abstract sig IPort extends Port{} abstract sig OPort extends Port{flow: set IPort,} abstract sig Function{input: set IPort,output: set OPort,status: Status}Figure 2: Case study metamodel (simplified)We then define instances of these concepts corresponding to the LPV functional architec-ture. The function instances take into account the selection of the source by the crew (SelectSource),the satellite data position (GPSand Galileo), two occurrences of SBAS positioning (ComputeSBAS1,ComputeSBAS2), two occurrences of LPV processing (ComputeLPV1, ComputeLPV2), threeoccurrences of displays (Acquirei, i2f1..3g), three occurrences of display resetters (Crosschecki,i2f1..3g) and of monitors in order to trigger an alarm, (Monitori, i2f1..3g). We also define thedifferent ports of each function, and the way ports are related to each other via flows. For in-stance, the following Alloy code is an excerpt of the flow definition, expressing that the outputport oSBAS1is related to the input port iSBAS1via a flow (idem for oSBAS2and iSBAS2).flow= oSBAS1!iSBAS1+oSBAS2!iSBAS2+...We also define some global constraints the architecture must satisfy, such as the fact thattwo ports related by a flow share the same status and the same value: