Version: 1 - Software Plattform Embedded Systems...

38
D-AV-3.2C: Verfahren zu Time & Space Partitioning Version: 1.0 Projektbezeichnung SPES 2020 Verantwortlich Dr. Rupert Reiger QS-Verantwortlich Dr. Stephan Stilkerich Erstellt am 10.07.2011 Zuletzt geändert 09.01.2012 Vertraulich für Partner: Alle Partner Projektöffentlich Freigabestatus X Öffentlich in Bearbeitung vorgelegt Bearbeitungszustand X fertig gestellt

Transcript of Version: 1 - Software Plattform Embedded Systems...

Page 1: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C: Verfahren zu Time & Space Partitioning

Version: 1.0

Projektbezeichnung SPES 2020

Verantwortlich Dr. Rupert Reiger

QS-Verantwortlich Dr. Stephan Stilkerich

Erstellt am 10.07.2011

Zuletzt geändert 09.01.2012

Vertraulich für Partner: Alle Partner

Projektöffentlich

Freigabestatus

X Öffentlich

in Bearbeitung

vorgelegt

Bearbeitungszustand

X fertig gestellt

Page 2: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

2

Weitere Produktinformationen

Erzeugung Dr. Rupert Reiger

Mitwirkend

Änderungsverzeichnis

Änderung

Nr. DatumVersi

on

GeänderteKapitel

Beschreibung der Änderung Autor Zustand

1 10/07/11& folgendeWochen

0.1 alle Initiale Produkterstellung,alle Belange zum Thema

sammeln

Reiger InBearbeitung

2 30/07/11& folgendeWochen

0.2 alle Literaturrecherche Reiger InBearbeitung

3 12/08/11& folgendeWochen

0.3 alle Stand der Technik Reiger InBearbeitung

4 25/09/11& folgendeWochen

0.5 alle Prinzip der StudieStruktur

Reiger InBearbeitung

5 31/09/11& folgendeWochen

0.7 alle GliederungKeywords

Bilder

Reiger InBearbeitung

6 12/10/11& folgendeWochen

0.85 alle Tailoring, Struktur finaleVersion,

Stichpunkte in Prosa

Reiger InBearbeitung

7 15/10/11& folgendeWochen

0.86 schreiben Reiger InBearbeitung

8 30/10/11& folgendeWochen

0.87 schreiben Reiger InBearbeitung

9 09/01/12& folgendeWochen

0.90 schreiben Reiger InBearbeitung

10 09/01/12 0.99 Fertigstellung Reiger final

11 09/01/12 0.999 QA Stilkerich final

12 09/01/12 1.00 Fertigstellung Reiger final

Page 3: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

3

Kurzfassung

Verfahren zu Time & Space Partitioning beinhaltet:

2) Discussion of Partitioning in Avionics Architectures & the Aspect of Certification

That is to understand IMA an basis for the methods.

3) (Non-) Functional Requirements - Qualities

That is to understand safety requirements from aeronautics

4) The ARINC Standard defines the Architecture

The standards to apply

5) Scheduling in the IMA Standard

A core problem to model

6) What is Synthesis, what must be modeled?

The principles of model based and IMA

7) Methods

The theory behind the scenery

8) Ensuring intra- and inter-IMA Communication

A little overview about some tools

Page 4: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

4

Document:

Index

1 Positioning and Abstract .................................................................................. 5

1.1 Motivation..................................................................................................... 51.2 Management Summary ................................................................................ 5

2 Discussion of Partitioning in Avionics Architectures & the Aspect ofCertification............................................................................................................... 6

2.1 Mechanisms and Assurance ........................................................................ 62.2 System Considerations & Standards ARINC 653 and DO-178B.................. 6

3 (Non-) Functional Requirements - Qualities.................................................... 7

4 The ARINC Standard defines the Architecture ............................................... 8

5 Scheduling in the IMA Standard..................................................................... 11

6 What is Synthesis, what must be modeled? ................................................. 13

6.1 Strongly Cyclic Major Time Frames............................................................ 166.2 Minor Time Frames - Partition Management: ............................................. 166.3 Processes in partitions: .............................................................................. 166.4 Communication: ......................................................................................... 176.5 Temporal Constraints / the scheduling task:............................................... 176.6 Spatial Constraints: .................................................................................... 17

7 Methods............................................................................................................ 19

7.1 Model Checking.......................................................................................... 197.2 Rich Component Models - Assumptions - Promises .................................. 207.3 Composing Components and analyzing Capability: Using Rich Components

227.4 Composing Components: The CMU SEI PACC Method ............................ 24

8 Ensuring intra- and inter-IMA Communication ............................................. 30

Page 5: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

5

1 Positioning and Abstract

1.1 Motivation

Das Dokument behandelt die Verfahren zur Erstellung von Avionik-Software nachdem Prinzip der Integrierten Modularen Avionic (IMA). Diese Systeme haben denVorteil der garantiert wechselwirkungsfreien gemischten Kritikalität von Prozessenauf einem Prozessor (time partitioning) sowie der wechselwirkungsfreien Verteilungvon Prozessen auf mehrere Prozessoren (space partitioning), letzteres geschieht ausmehreren Gründen wie der Replikation zur Minimierung von Ausfallwahrscheinlich-keiten.

IMA Systeme sind klar strukturiert und übersichtlicher wie „federated systems“, dieSoftware ist besser wartbar und austauschbar und Hardware ist durch time partitio-ning besser genutzt. Ausfallsicherheit wird durch space partitioning und Replizierunggewährleistet.

Zu Verfahren zur Erstellung von IMA Systemen gibt es den modellgestützten Sys-tementwurf als Stand der Technik. Dadurch wird die frühzeitige Verifikation und Vali-dierung von Architekturen ermöglicht und die Grundlage für rechtzeitige und flexibleKorrekturen geschaffen, wobei durch ständige automatische Prüfung die Konsistenzgewährleistet ist.

1.2 Management Summary

Das Dokument behandelt Modellierung und Erstellung von IMA Systemen. Es folgtdabei einer Sublösung des Problems d.h. deterministischen Systemen, da diese mitvertretbarem Aufwand zertifizierbar sind.

Jede IMA besitzt „zumindest“ time-partitioning – durch die für sicherheitskritischeSysteme notwendige Replizierung von Prozessen ergibt sich zwangsweise dasspace-partitioning.

Baut man ein Avioniksystem, geht es um das Einhalten der funktionalen sowie dernichfunktionalen Requirements. Hier behandeln wir das Sicherstellen der nichtfunkti-onalen Requirements. Die nichtfunktionalen Requirements sind für sicherheitskriti-sche Echtzeitsysteme der Ausgangspunkt von allem folgenden.

Die Basis der Abhandlung ist der ARINC 653 (Avionics Application Standard Soft-ware Interface) Standard, das ist eine Software-Spezifikation für „space- and timepartitioning“ in sicherheitskritischen Echtzeitsystemen für Integrierte Modulare Avio-nik (IMA).

Page 6: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

6

2 Discussion of Partitioning in Avionics Architectures &the Aspect of Certification

2.1 Mechanisms and Assurance

A centralized IMA architecture must provide replicated and physically distributedhardware for fault tolerance, together with mechanisms for redundancy management.So a conceptually centralized IMA will be, internally, a distributed system.

The traditional federated architecture is a major obstacle to a rational organization offlight functions, and IMA is the best hope for removing this obstacle. That suggestsexamining partitioning for IMA as a distributed system in which flight functions areeach allocated to separate processors, replicated as necessary for fault tolerance. Inthis model it is to limit fault propagation between the processors supporting eachfunction, but not within them.

If functions have no internal partitioning, then all their software must be assured andcertified to the level appropriate for that function. Thus, all the software in an autopilotfunction is likely to require assurance to Level A of DO-178B if part of it has that re-quirement.

With IMA partitioning within a processor could allow an individual function to be di-vided into software components of different criticalities; each could then be devel-oped and certified to the level appropriate to its criticality.

It is described Spatial partitioning and Temporal/Time partitioning and how to doit and what to take care for.

2.2 System Considerations & Standards ARINC 653 and DO-178B

Several IMA system design challenges are posed by common hardware featuressuch as interrupts, Direct Memory Access (DMA), and system Input/Output (I/O),as they may produce unpredictable distortions that violate the constraints of time andspace partitioning.

Time and space partitioning must be deterministic in an ARINC 653-based IMA sys-tem in order to avoid aircraft certification concerns and incompatibilities with the stan-dards and guidelines set forth in DO-178B. Methods for identifying, analyzing, andrectifying potential determinism issues in the IMA system are presented herein.

As described robust time partitioning “must ensure that the service received fromshared resources by the software in one partition cannot be affected by the softwarein another partition the performance of the resource concerned, as well as the rate,latency, jitter, and duration of scheduled access to it”

For that it has to be dealt with

Potential Issues with DMA Transfers in Robustly-Partitioned IMA Systems

Potential Issues with Interrupts in Robustly-Partitioned IMA Systems

Potential Issues with I/O in Robustly-Partitioned IMA Systems

Page 7: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

3 (Non-) Functional Requirements - Qualities

Computational models pure synchronous models

partially synchronous models

asynchronous models

pure asynchronous models

Data models shared data

access modes

data types

process bindings

data partitioning

Process models structures, graphs

starting, terminating, suspending, aborting

interrupts

serializability, transactions

failures, vitality

resource preemtion

WCET

Computational modelsComputational models pure synchronous modelspure synchronous models

partially synchronous modelspartially synchronous models

asynchronous modelsasynchronous models

pure asynchronous modelspure asynchronous models

Data modelsData models shared datashared data

access modesaccess modes

data typesdata types

process bindingsprocess bindings

data partitioningdata partitioning

Process modelsProcess models structures, graphsstructures, graphs

starting, terminating, suspending, abortingstarting, terminating, suspending, aborting

interruptsinterrupts

serializability, transactionsserializability, transactions

failures, vitalityfailures, vitality

resourceresource preemtionpreemtion

WCETWCET

Event models & arrival models event / process bindings

periodic

sporadic

aperiodic

arbitrary

Failure models always correct

intermittently

permanently

time domain:

clean crash

crash with pollution

past states lost / accessible

omission

early timing / late timing

Byzantine

Failure occurrence models sporadic

aperiodic

unimodal arbitrary

multimodal arbitrary

Event models & arrival modelsEvent models & arrival models event / process bindingsevent / process bindings

periodicperiodic

sporadicsporadic

aperiodicaperiodic

arbitraryarbitrary

Failure modelsFailure models always correctalways correct

intermittentlyintermittently

permanentlypermanently

……

time domain:time domain:

clean crashclean crash

crash with pollutioncrash with pollution

past states lost / accessiblepast states lost / accessible

omissionomission

early timing / late timingearly timing / late timing

ByzantineByzantine

……

Failure occurrence modelsFailure occurrence models sporadicsporadic

aperiodicaperiodic

unimodalunimodal arbitraryarbitrary

multimodal arbitrarymultimodal arbitrary

Logical safety nothing bad happens set of invariants shall never be

violated:

causal process ordering

atomicity

transactions

mutual exclusion

data consistency

process serializability

Liveness something can always happen

process eventually terminates in the absence of

conflicts

no deadlocks

no starvation

no livelocks

Timeliness something good happens in finite, bounded, predictable time

real time

timeliness constraints

earliest / latest start time

earliest / latest deadline

l inear / non linear function of system state

Logical safetyLogical safety nothing bad happensnothing bad happens set of invariants shall never beset of invariants shall never be

violated:violated:

causal process orderingcausal process ordering

atomicityatomicity

transactionstransactions

mutual exclusionmutual exclusion

data consistencydata consistency

process serializabilityprocess serializability

LivenessLiveness something can always happensomething can always happen

process eventually terminates in the absence ofprocess eventually terminates in the absence of

conflictsconflicts

no deadlocksno deadlocks

no starvationno starvation

nono livelockslivelocks

TimelinessTimeliness something good happens in finite, bounded, predictable timesomething good happens in finite, bounded, predictable time

real timereal time

timeliness constraintstimeliness constraints

earliest / latest start timeearliest / latest start time

earliest / latest deadlineearliest / latest deadline

linear / non linear function of system statelinear / non linear function of system state

Dependability system behavior in presence of partial failures

space / time redundancies

combines safety and liveness

reliability

availability

fault tolerance / replications

safety / safety chains

security / immunity to attacks

process atomicity execution-wise

atomic commit terminat ion-wise

reliable broadcast

causal broadcast

atomic broadcast

agreements

consensus

Security

DependabilityDependability system behavior in presence of partial failuressystem behavior in presence of partial failures

space / time redundanciesspace / time redundancies

combines safety and livenesscombines safety and liveness

reliabilityreliability

availabilityavailability

fault tolerance / replicationsfault tolerance / replications

safety / safety chainssafety / safety chains

security / immunity to attackssecurity / immunity to attacks

process atomicityprocess atomicity executionexecution--wisewise

atomic commitatomic commit terminationtermination--wisewise

reliable broadcastreliable broadcast

causal broadcastcausal broadcast

atomic broadcastatomic broadcast

agreementsagreements

consensusconsensus

SecuritySecurity

F

Figure 2: Models

7

igure 1: non-functional requirements / qualities

Page 8: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

8

In systems, software engineering and requirements engineering, non-functional re-quirements are requirements that specify criteria that can be used to judge the opera-tion of a system, rather than specific behaviors. This should be contrasted with func-tional requirements that specify specific behavior or functions. In general, functionalrequirements define what a system is supposed to do whereas non-functional re-quirements define how a system is supposed to be. Non-functional requirements areoften called qualities of a system. Other terms for non-functional requirements are"constraints", "quality attributes", "quality goals" and "quality of service requirements".Qualities about non-functional requirements can be divided into two main categories:

Evolution qualities, such as testability, maintainability, extensibility and scalabil-ity, are embodied in the static structure of the software system. As they are lessspecial IMA as the execution qualities, they are dropped for further discussion.

Execution qualities, such as logical safety, liveness, timeliness, special depend-ability constructs, security and usability, are observable at run time.

Examples for Execution qualities are:

Safety: “something bad will not happen.” in contrast to the “bad thing is irreme-diable”,

Liveness: “something good will eventually happen.” “it remains possible for thegood thing to occur”, liveness is the major challenge in model checking, and as ageneral real-time non-functional requirement

Timeliness: “something good happens in finite, bounded, predictable time” “realtime” so real time does not mean that something is especially fast but predictable.

Safety, liveness and timelines are the central requirements to me modeled.

Keeping requirements especially the non-functional is the key task of the time& space partitioning methods

4 The ARINC Standard defines the ArchitectureARINC 653 (Avionics Application Standard Software Interface) is a software specifi-cation for space- and time-partitioning in safety-critical avionics real-time operatingsystems. It allows hosting multiple applications of different software levels on thesame hardware in the context of Integrated Modular Avionics (IMA).

In order to decouple the RTOS platform from the application software, ARINC 653defines an API for space and time partitioning.

ARINC 653 provides the following services through its API:

Partition Management

Process Management

Time Management

Interpartition Communication

Intrapartition Communication

Health Monitoring

Page 9: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

9

Figure 3: Time- (horizontally) and Space- (vertically) partitioning

An ARINC 653 platform contains:

A hardware allowing (!) Real-time computing deterministic services.

An abstraction layer managing the timer and space partitioning constraints of theplatform (memory, CPU, Input/output).

An implementation for the ARINC 653 services (the APEX API).

An interface to be able to configure the platform and its domain of use.

Various instrumentation tools.

Page 10: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

10

ARINC 653 compliant IMA requirements for Modeling-Syntax and –Semantics,for hard RT-Systems, determinism add constraints:

For space partitioning (virtual & non-virtual): The protection of Program, data, registers and Dedicated I/O.

Further that persistent storage / memory is writable by one partition, That temporary storage location / registers of a partition are saved when control is

transferred.

For time partitioning: Protection of processing and communications bandwidth assigned to a partition, Partition’s access to a prescribed set of hardware resources for a prescribed period of

time is guaranteed, The order of execution between communicating partitions is consistent each execu-

tion frame, and that results in a Defined execution of the threads contained in the correlated process of the partition, Every thread gets its CPU resources every period.

So in general, no Functional Partition may: Contaminate another’s code, I/O, or data storage areas, Consume shared processor resources to the exclusion of any other partition, Consume I/O resources to the exclusion of any other partition, Cause adverse affects to any other partition as a result of a hardware failure unique

to that partition.

So with IMA, the RTOS has to take care for: Non-preemptive multitasking, Rate monotonic scheduling with priority inheritance in case of interrupt driven

threads, Dynamic threads, scheduling, mutual exclusion, Space partitioning for processes, Time partitioning for threads, Aperiodic interrupt threads, if allowed, Overhead accounting in scheduler & slack.

The programmer has to take care for: The threads being deadlock free, That data are written before read, That no data races occur.

NNoowwhheerree tthhrroouugghhoouutt tthhee IIMMAA AArrcchhiitteeccttuurree aa ssiinnggllee ppooiinntt ooff ffaaiilluurree iiss aalllloowweedd

Page 11: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

11

5 Scheduling in the IMA StandardThe ARINC 653 specification defines a general purpose APEX (Applica-tion/Executive) interface between the OS and the application software.

Figure 4 is explaining time partitioning and frames on the time axis; for the wordingconcerning frames, ARINC 653 defines frames (major) and partitions (being contain-ers for processes) and APEX defines major frames and minor frames (= partitions)being containers for processes, being the main parameters of a partitioned system.So Figure 4 shows a realization of the IMA requirements above with respect to parti-tions and scheduling, delivering the parameters for a schedule-optimizing tool.

M ajor Tim e Fram e

P artition 1 P artition 2 Pa rtition 3 Partition 1 Pa rtitio n 2 Partition 1 Partition 2

= P artition Id le

T imet1 t2 t3t0 t6

t1P1

t2P1

t3P 1

t1P1

t2P 1

t 3P 1

t1P 1

t2P 1

t3P1

t1P 2

t2P 2

t1P 3

t 2P 3

t3P3

t1P 2

t2P2

t1P2

t2P2

Minor Tim e Fram e

t4

M ajor Tim e Fram e

P artition 1 P artition 2 Pa rtition 3 Partition 1 Pa rtitio n 2 Partition 1 Partition 2

= P artition Id le

T imet1 t2 t3t0 t6

t1P1

t2P1

t3P 1

t1P1

t2P 1

t 3P 1

t1P 1

t2P 1

t3P1

t1P 2

t2P 2

t1P 3

t 2P 3

t3P3

t1P 2

t2P2

t1P2

t2P2

Minor Tim e Fram e

t4

P “2” P “1” P”2”P “3” P “1”P “3”spare spareP “1” P “3”Process “1”

Minor Frame “1”

P “4” spare

Major Frame Major Frame Major Frame

Minor Frame “2” Minor Frame “3”

tP “2” P “1” P”2”P “3” P “1”P “3”spare spareP “1” P “3”Process “1”

Minor Frame “1”

P “4” spare

Major Frame Major Frame Major FrameMajor Frame Major Frame Major Frame

Minor Frame “2” Minor Frame “3”

t

Figure 4: Time partitioning in the time axis; partitions are minor time frames which can haveseveral tasks

1 2 3

1http://yunus.hacettepe.edu.tr/~ki/dersler/bbs671/Sunu%20Onerileri%20ve%20Projeler/safety-critical-sw-dev_wp.pdf

2vxworks_653_programmers_guide_2.1

3Präsentation Joachim Hampp, VxWorks MILS, Wind River

Page 12: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

12

Figure 5 shows the parts of the ARINC 653 API doing the job, eachred box exactly containing the parameters to be determined to de-fine the system, following the tree from top to bottom and from leftto right:

Sam pling

API

Sem aphore

Blackboard

Buffer

Queuing

M em oryM anagem ent

Comm unicationM anagem ent

ProcessM anagem ent

Inter-Parti tion

Tim eM anagem ent

PartitionM anagem ent

Intra-Parti tion

P eriodic

A periodic

M essagevia Port

M essage

S ynchron isationEvent

HealthM onitoring

M essage viaLogbook

Figure 5: ARINC 653 API delivers the IMA parameters to be determined to define the system

The main task building the IMA system is to get a time determinismbased schedule for space partitioning and time partitioning that isfor all “processes in minor frames” and for all “minor frames in ma-jor frames” the latter finally strongly periodic, all so as to fulfill allintrapartition and interpartition communications of all kind so asperiodic, aperiodic, via synchronization or messaging and further tofulfill all memory access parameters as well as all nonfunctional pa-rameters from the specification.

Example:As explained partitions can comprise one or more processes, in which a process is afunctional thread. A priority pre-emptive scheduling mechanism, managed by the op-erating system, determines the manner in which processes are executed.

A typical realization of a Time Partitioning Scheduler (TPS) is: IMA-OS scheduler for partitions,

Page 13: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

13

Intra-partition scheduling use priority pre-emptive scheduling e.g. see APEX,POSIX, etc.

It must be possible to model this architectures and behavior from ARINC 653 APIparameters.

From above this implies that processes can have different performance require-ments, which split into two categories:Rate requirements and response requirements: Rate requirement where a task must provide service at a particular rate (so pe-

riodic in Figure 5). Response requirement when an event occurs, the task responds to it within a

certain amount of time (so a periodic in Figure 5).That is partition internal business, so the partition is responsible for its internal proc-ess behavior. Neither the process nor its attributes are visible outside of the partition.

6 What is Synthesis, what must be modeled?It is mentioned here that for hard real-time systems determinism is the major parame-ter and derived from section 3 “(Non-) Functional Requirements - Qualities”.That is not, that determinism follows directly from non-functional requirements, butthe other way around: For deterministic systems it’s easier to show to fulfill non-functional requirements, e.g. timely constraints. In principle any system, synchro-nous, asynchronous, allowing interrupts, etc. could fulfill given non-functional re-quirements, but showing and so validating that normally is far beyond a complexitybeing mastered by man using any tools.

Note: A system is deterministic or not, there is no between. When determinism is vio-lated at any point, the system is not deterministic. In practice a system is determinis-tic, when it’s proven to be deterministic, otherwise it is not.

A system-wide perspective is necessary when designing the IMA solution in order toensure robust time and space partitioning is preserved during normal operation.Time and space partitioning must be deterministic in an ARINC 653 based IMA sys-tem in order to avoid aircraft certification concerns and incapability with the standardsand guidelines in DO-178B. Methods for identifying, analyzing, and rectifying deter-minism in IMA systems are to be used.

How does synthesis follow the parameters?What are the major issues?

Several IMA system design challenges are interrupts, direct memory access (DMA),system I/O, as they can produce unpredictable distortions that violate the constraintsof time and space partitioning, best protected by determinism as a sufficient condi-tion4. DMA: In comparing standard memory transactions with DMA transactions, it

should be evident that the transaction efficiency provided by DMA engines pro-vides a powerful means of transferring large blocks of memory within the system;

4Justin Littlefield-Lawwill, GE Aviation, Grand Rapids, Michigan, Larry Kinnan, Wind River Systems,Alameda, California: SYSTEM CONSIDERATIONS FOR ROBUST TIME AND SPACEPARTITIONING IN INTEGRATED MODULAR AVIONICS

Page 14: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

however, the power afforded by the DMA engine is not without potential ramifica-tions to robust partitioning. Since the DMA engine is granted exclusive access tothe memory bus to perform a block transfer, and since the memory bus is a re-source that is shared by the entire IMA system, there exists an opportunity for onepartition to deprive another partition of a critical resource it needs to execute if theshared resource is not made available to the subsequent requestor.

DbpDp

Partition ASpace

Partition BSpace

Partition CSpace

20 ms

MinorFrame

200 msMajorFrame

Time

. . .

Partition ASpace

Controls

Application

ControlsTask

System

Application

SystemManagement

Task

Input/OutputManagement

Task

Resource Monitor

Application

Resource MonitorTask

Controls

Application

ControlsTask

80 ms

MinorFrame

100 ms

MinorFrame

Initiate DMATransfer@ 60 ms

40 ms DMATransfer

Time

VIOLATION

20 ms Temporal Violation,80 ms Remain For Partition C

Partition ASpace

Partition BSpace

Partition CSpace

20 msMinorFrame

200 msMajor

Frame

Time

ContextSwitchPoint

. . .

Partition ASpace

ControlsApplication

ControlsTask

SystemApplication

SystemManagement

Task

Input/OutputManagement

Task

Resource MonitorApplication

Resource MonitorTask

ControlsApplication

ControlsTask

80 msMinorFrame

100 msMinorFrame

F

14

MA-induced temporal violations occur whenever a DMA transfer is initiatedy a partition that has less execution time remaining than the time required com-leting the DMA transfer. Expressed mathematically, the time to complete theMA transfer must be less than the partition duration less the time already ex-ended by the partition in order to avoid violating robust temporal partitioning.

igure 6:4

Robust Partitioning Impacted by DMA-Induced Temporal Violation

Page 15: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

15

Interrupts: In general, a processor interrupt is caused by an external signal whichtriggers an asynchronous event in the system where normal operation is sus-pended, and processing is redirected to a piece of software that handles or ser-vices the interrupt event. When a processor interrupt is enabled and the interruptevent occurs, the processor must switch contexts to a space defined by the inter-rupt vector and a time specified by the execution duration of the interrupt handlersoftware routine.But in highly critical IMA following ARINC 653 the only interrupt typically found ina robustly-partitioned system is the system clock, and this is for good reason.The RTOS in the IMA system must be in complete control of temporal and spatialcontexts in order to guarantee robust partitioning, and interrupts present thethreat of injecting an unpredictable, independent context into the system that redi-rects normal operation, destroying determinism. While interrupts may provide aconvenient method of forcing the system to handle some high-priority externalevent, handling interrupts in the IMA system may cause distortions in the tempo-ral domain that enervate robust partitioning.In case of interrupts when context is restored, the time spent handling the inter-rupt is accounted for by the interrupted partition, since any readjustment of thepartition’s original execution timeline may introduce an unacceptable amount ofjitter into the system and violate the strict scheduling requirements given inARINC 653. Thus as a consequence of strict scheduling, if the global interrupthandler’s duration exceeds the execution time remaining in the interrupted parti-tion, execution time will be accounted for by the subsequent partition(s).Interrupt-induced temporal violations occur whenever an interrupt other thanthe system clock interrupt occurs during the normal execution schedule of thesystem. Interrupts could be caused by external events such as I/O operationstranspiring or perhaps might even be caused by activity directly initiated by thepartition application. Externally-caused interrupt activity might not be forbidden inprinciple but is especially problematic for the IMA system since there may be nomethod to completely analyze or characterize the activity unless it is peri-odic in nature and even more being deterministic.In general, ARINC 653 partitioned operating systems tend to avoid use of inter-rupts aside from the system clock. Systems that do employ interrupts typicallyuse a combination of all of the aforementioned techniques in order to achieve alevel of determinism consistent with the criticality level they will be certified for.

I/O: I/O in a partitioned IMA system presents the developer with one of their mostchallenging aspects of design. While ARINC 653 clearly defines operations andinterfaces for inter-partition I/O via ARINC sampling or queuing ports, I/O tophysical devices or inter-module I/O are left to RTOS implementers and otherstakeholders to provide. As discussed previously, use of interrupts cancause temporal violations in the IMA system due to their asynchronous na-ture. The removal of asynchronous behavior from the system tends to driveI/O solutions towards either polling-mode software operations or towards ahardware-based design. The polling–mode solution clearly introduces a limit tothe bandwidth of the I/O data that may be processed and also increases the la-tency of response; therefore, the solution must be analyzed for acceptable per-formance. Ideally, the architecture of the I/O solution would try to isolate any I/Oaccess to a single partition-based I/O implementation in order to afford the maxi-mum benefit of partitioning. Such I/O architecture defines the “classical” I/O parti-tion model that is usually the first choice of designers when confronted with a par-titioned system. The primary limitation of the classical I/O partition solution is that

Page 16: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

16

the I/O bandwidth will be limited by the frequency at which the I/O partition isscheduled in the major frame. Depending on the data rate required, the classicalI/O partition model may not be acceptable since the necessary periodicity of theI/O partition may be too high to be accommodated by the overall system sched-ule.I/O-induced temporal violations can occur for a number of reasons as previ-ously discussed, and in general, such violations are typically remedied either byavoiding potentially temporally unsafe operations or by designing sufficient intelli-gence into the drivers to prevent them from occurring. E.g. from a performancestandpoint, it is desirable to transfer data to driver memory space (buffer) and al-low the application to continue operating, with the expectation of a process sub-sequently transferring the data from driver memory space to the device.

6.1 Strongly Cyclic Major Time Frames

Major time frames are scheduled strongly cyclic (round robin) and deterministic.

6.2 Minor Time Frames - Partition Management:

Partitions can be of different criticality (e.g. with respect to ARINC 653). They areexecuted cyclically in a strict order. This order is also called partition time frame,which is configured at the system configuration time and repeated cyclically.Every partition is assigned a fixed duration, i.e. allowed execution time, and pe-riod, i.e. a time point of partition activation within a frame/cycle.

By cyclic scheduling of partitions, if a partition does a restart, it will restart fromthe last saved position. When the partition is in context, the processes will con-tinue where they last left off. The scheduler does not restart scheduling processeswith respect to partition-internal processes each time the partition is in context.This enables continuation of the application within real-time.

6.3 Processes in partitions:

That is what is possible in principle, but following ARINC 653 for highly criticalsystems, determinism is to be followed also inside the partitions and polling is tosubstitute interrupts so also avoiding aperiodic processes.

Each partition comprises one or more tasks/processes that combine dynamicallyto provide the functions associated with that partition. According to the character-istics associated with the partition, the constituent processes may operate concur-rently in order to achieve their functional and real-time requirements. Multipleprocesses are therefore supported within the partition.

Processes are designed for either periodic or non-periodic execution. There shallbe a mechanism that either starts a process again in case of an error, or termi-nates it or schedules it again. Partition or Process code may run only in usermode (of an underlying CPU). Therefore no privileged instructions can be exe-cuted.

Each process has a priority level. If a partition is active, the process of the highestpriority within the partition is selected and executed. When a partition is resched-uled, the sequence of processes is started in a state as it was saved as the proc-esses have been pre-empted as the partition was replaced by another cyclically.Ruling all processes having finished execution at any one time inside each parti-tion and so before cyclic replacement of the partition is a simplified, prevalent andcomprehensive variant.

Periodic processes: they have a constant time interval between successiverequests.

Page 17: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

17

Aperiodic process: neither the processes request time nor the minimum timeintervals between successive requests are known. They have to be under the ruleof deterministic strong periodicity corset and have to be overruled by the clockdriven interrupts.

6.4 Communication:

Inter partition communication: Communications between individual partitions.Buffers and blackboards are provided for general inter-process communication(and synchronization); semaphores and events are provided for inter-processsynchronization.

No partition is allowed to influence another partition via technical communicationmeans in any case, for example influencing timing via synchronization etc.

So communication between partitions is done by means of messages. Sourceand destination of a message are always partitions, not processes. Processescan access the ports according to their need, but the ports always belong to parti-tions. A message can be sent or received via a port. How the messages aretransferred, is determined in the configuration tables of the module. There are twomodes the ports operate in sampling mode (message is in port till transferred oroverwritten) and queuing mode (no overwriting).

Intra partition communication: That is communication strictly inside a partition.The intra-partition communication mechanisms are buffers, blackboards, sema-phores, events, and global variables. All intra-partition message passing mecha-nisms must ensure atomic message access.

So, processes use inters partitions (queuing/sampling ports) and intra parti-tions (buffer/blackboard/semaphore/event) communication resources to ex-change data.

6.5 Temporal Constraints / the scheduling task:

Temporal constraints are described using partition and process attributes. Period andduration are statically defined partition attributes.It is to separate activities into real-time and non-real-time tasks, where each kind oftask shall have specific constraints for designing and testing. In separate partitionsreal-time and non-real-time can run on one system. Common sequencing mecha-nisms used is sequential tasking and multi tasking.The temporal segregation managed by the operating system guarantees that eachpartition keeps its own timing without being disrupted by another partition

6.6 Spatial Constraints:

Partition’s data (e.g. of spatially separated partitions) cannot be modified by anotherpartition. This constraint would help to define the implementation of an application onone ore several partitions.By defining the memory management requirements of a partition and its processes atinitialization, the system can provide process-level protection of resources. This levelof protection could not easily be provided if processes were created during runtime,since it would require dynamic interaction with MMU hardware and its data structureswhen a process is created. This interaction would complicate the certification effortof the OS, while increasing the duration for that effort.

Page 18: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

Fig

5Al

18

ure 7 shows the IMA / AFDX example comprehending the points above5.

bert Benveniste (INRIA-IRISA, Rennes / COMBEST))

Figure 7: AFDX point to point to communication

Page 19: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

7 Methods

7

MtatinM

6

7

Safety: Formal Methods for dependable Systems, Process and VSafety: Formal Methods for dependable Systems, Process and V--ModelModel

preventionprevention removalremoval diagnosisdiagnosistolerancetolerance

WCET analysisWCET analysisWCET analysis

static analysis / abstract interpretation (AI)FP precision analysis

range checking

static analysis / abstract interpretation (AI)static analysis / abstract interpretation (AI)FP precision analysisFP precision analysis

range checkingrange checking

RTE analysisRTE analysisRTE analysis

model checkingstate machines

linear temporal logic (LCL)computation tree logic (CTL)

model checkingmodel checkingstate machinesstate machines

linear temporal logic (LCL)linear temporal logic (LCL)

computation tree logic (CTL)computation tree logic (CTL)

SpecificationsSpecificationsSpecifications

Designreplications (IMA)

DesignDesignreplications (IMA)replications (IMA)

CodingCodingCodingUnit testUnit testUnit test

IntegrationIntegrationIntegration

ValidationValidationValidation

schedulability analysisduration calculus (DC)

interval duration logic (IDL)

schedulability analysisschedulability analysisduration calculus (DC)duration calculus (DC)

interval duration logic (IDL)interval duration logic (IDL)

communicability analysisinfluence chains

network / real time calculusproved max latency

communicability analysiscommunicability analysisinfluence chainsinfluence chains

network / real time calculusnetwork / real time calculus

proved max latencyproved max latency

traceability

safety cases

traceability

traceability

safety cases

safety cases

SWdia

gnos

is

&m

onito

ring

code

inst

rum

enta

lizat

ion

SWdia

gnos

is

SWdia

gnos

is

&m

onito

ring

&mon

itorin

gco

deco

de

inst

rum

enta

lizat

ion

inst

rum

enta

lizat

ion

SW

diagnosis

&m

onitoring

f rom

symp

toms

tofailu

res

toerro

rs

tofau

lts

SW

diagnosisS

Wdiagnosis

&m

onitoring&

monitoring

f romsym

ptoms

fromsym

ptoms

tofailures

tofailures

toerrors

toerrors

tofaults

tofaults

WCET feedbackWCET feedbackWCET feedback

CertificationDO-178c

CertificationCertificationDODO--178c178c

formal requirementssafety cases

formal requirementsformal requirements

safety casessafety cases

UML RT profilecomponents / contracts

UML RT profileUML RT profilecomponents / contractscomponents / contracts

mod

elfe

edba

ckm

odel

feed

back

mod

elfe

edba

ck

Fa

igure 8: Overview of the main methods for non-functional requirements od dependable systems

.1 Model Checking6,7

odel checking is a formal verification technique for assessing properties of informa-ion and communication systems. Model checking requires a model of the systemnd a desired property and from that checks whether or nit the given model satisfies

he desired property. Typical properties that can be checked are deadlock freedom,nvariants and request-response properties. Model checking is an automated tech-ique to check the absence of errors.odel checking is built upon sound mathematical methods like:

SM (state machines)TS (transition systems)LTP (linear time properties, deadlocks, liveness)BA (Automata, Büchi Automata)LTL (linear temporal logic)CTL (computation tree logic)BisimulationTCTL (timed computation tree logic)

Christel Baier, Joost-Pieter Katoen / Model Checking ISBN: 978 0 262 02649 9Sharma, Pandya, Chakraborty / IITB, Tata Institute of Fundamental Research

nd their placement in the process

Page 20: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

20

IDL (interval duration logic) DC (duration calculus) BMC (bounded model checking) NT & RT (network- and real-time calculus).Model checkers are typically built on one or a couple of these theories. A lot can bedownloaded and used for building an IMA.

Focusing on model- and component-based IMA construction and IMA components communicationSeveral tools built on some of the above theories exist including tool support andtraining.

7.2 Rich Component Models - Assumptions - Promises8,9,10

We define

Rich Components8

A component: fully re-usable design artifact providing a well defined functionality Application level functionality “features” of application level functions – level of granularity determined by

need to customize application level function Middleware components Hardware components “Rich” Explicates all assumptions and/or dependencies on its design context following

that promises are guaranteed Such that assessment to functional and non-functional characteristics can be

made without assessing component itself Component Characterization For all viewpoints Safety, Reliability, Real-Time, Power, Bandwidth, Memory consumption,

behaviour, protocols

So a Rich Component has:

Assumptions reflect incomplete knowledge of actual design context Determine boundary conditions on actual design context for each view-point un-

der which component is promising its services are decorated with confidence levels Promises Are guaranteed if component is used in assumed design context Viewpoint specific models Explicate dependency of promises on actual guarantees by design context For all viewpoints Safety, Reliability, Real-Time, Power, Bandwidth, Memory consumption,

behaviour

8Werner Damm, Sylvain Prudhomme / OFFIS, Airbus: Controlling Speculative Design using

Rich Component Models9

Werner Damm, Angelika Votintseva, Alexander Metrner, Bernhard Josko, Thomas Peikenkamp,Eckehard Böde / OFFIS, Carl von Ossietzky Universität Oldenburg: Boosting Re-use of EmbeddedAutomotive Applications Through Rich Components10

Albert Benveniste, Benoît Caillaud, Roberto Passerone / INRIA, University of Trento:Multi_Viewpoint State Machines fpr Rich Component Models

Page 21: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

21

The Rich Component Model has 3 Views:

1. Functional View:

Horizontal assumption: Environment will provide the requested data Vertical assumption: The communication layer guarantees the transmission of

every message

2. Real Time View:

explicate dependency of promises on actual guarantees by design context forreal-time properties using Live Sequence Charts

Horizontal Assumptions: Requested information will be delivered within a speci-fied time frame

Vertical Assumptions: Worst case execution time is within a specified range

3. Safety View:

explicate propagation of failures in a conceptual model for a preliminary safetyassessment

Horizontal Assumptions: Failure modes/rates for required information Vertical Assumptions: Failure rates for each failure mode

A Rich Component has Interfaces: Interface Definition:

A group of services the component is ready to perform and services used by thecomponent

Static Description – Data: attributes, the values of which are exchanged (read or written) by the component

and its environment signals the component is ready to receive from or emit to its environment (asyn-

chronous) operation calls the component is ready to accept or invoke from its environment

(synchronous) Directions: Interface direction: horizontal orvertical, vertical = { up, down } Data directions: input or output Dynamic Description =Specifications containing perviewpoint Declarative specifications

(temporal) logic

Sequence DiagramsAnd/or

Automata suitably tailored to specific viewpoints

Property “kinds” Assumptions Promises

Page 22: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

So it is to look for formal methods like Automata and temporal logic, to address non-

functional requirements as illustrated in8:

7

Tp

F

F

F

.3 Composing Components and analyzing Capability: Using RichComponents10

he chapter is about analyzing non-functional system construction from Rich Com-onents.

igure 10 and Figure 11 show the principle.

igure 9: Rich Components and non-functional Requirements

22

igure 10: Rich Components Analyzing Compatibility

Page 23: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

Famdosmootis

TnCttcohf

Twosmp

23

ollowing10 the IP-SPEEDS Heterogeneous Rich Component (HRC) metamodel, itsssociated multiple viewpoint contract formalism and the underlying mathematicalodel of state machines supporting such contracts. Here each supplier is assigned aesign task in the form of a goal, which we call guarantee or promise that involvesnly entities for which the supplier is responsible. Other entities entering the sub-ystem for design are not under the responsibility of this supplier. Nonetheless, theyay be subject to constraints assigned to the other suppliers that can therefore beffered to this supplier as assumptions. Assumptions are under the responsibility ofther actors of the OEM/supplier chain but can be used by this supplier to simplify

he task of achieving its own promises. This mechanism of assumptions and prom-es is structured into contracts.

he model is based on the concept of component here heterogeneous rich compo-ents (HRC). A component is a hierarchical entity that represents a unit of design.omponents are connected together to form a system by sharing and agreeing on

he values of certain ports and variables. A component may include both implementa-ions and contracts. An implementation M is an instantiation of a component andonsists of a set P of ports and variables (in the following, for simplicity, we will refernly to ports) and of a set of behaviors, or runs, also denoted by M, which assign aistory of “values” to ports. Because implementations and contracts may refer to dif-

erent viewpoints.

he model build on the notion of a contract for a component as a pair of assertions,hich express its assumptions and promises. An assertion E is a property that mayr may not be satisfied by a behavior. Thus, assertions can again be modeled as aet of behaviors over ports, precisely as the set of behaviors that satisfy it. An imple-entation M satisfies an assertion E whenever they are defined over the same set oforts and all the behaviors of M satisfy the assertion.

Figure 11: Rich Components Vertical Analysis following Figure 10

Page 24: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

Accptt

Ttco

ThtG

Epc

7

P

B

o

P

1

M: implementationP: portsE: assertionC = (A,G): contract is an assertion withA: assumption, spec., requirementsG: promise (G from guarantee) <- also behavior

Promise G is subject to or depending on assumption A

An implementation M of a component satisfies a contract C wheneverit satisfies its promise G,subject to the assumption (spec.) A.

MC = G U ¬A.

24

contract is an assertion on the behaviors of a component (the promise) subject toertain assumptions. We therefore represent a contract C as a pair (A, G), where Aorresponds to the assumption, and G to the promise. An implementation of a com-onent satisfies a contract whenever it satisfies its promise, subject to the assump-

ion where M and C have the same ports. We write M |= C when M satisfies a con-ract C.

he combination of contracts associated to different components can be obtainedhrough the operation of parallel composition. If C1 = (A1, G1) and C2 = (A2, G2) areontracts, the composite must satisfy the guarantees of both, implying an operationf intersection.

he situation is more subtle for assumptions. Suppose first that the two contractsave disjoint sets of ports. The assumption and the promise of the composite con-

ract C = (A, G) can therefore be computed as A = (A1 ∩ A2) U ¬(G1 ∩ G2) and G =1 ∩ G2.

xtended State Machines (ESM) is to be used here for checking because of the sim-licity of its associated parallel composition in their adapted form HRC State ma-hines (URCSM).

.4 Composing Components: The CMU SEI PACC Method11

redictability by Construction:

uilding high-stakes systems from certified software components

r

redictable Assembly from Certifiable Components (PACC)

1Linda M. Northrop / CMU SEIPredictability by Construction: PACChttp://www.sei.cmu.edu/predictability/http://www.sei.cmu.edu/library/assets/pacc.pdfSoftware Product LinesISBN-13: 978-0201703320

¬A denotes the set of all runs, that are not runs of A.

Page 25: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

25

It is to fast assemble new and innovative software-intensive systems for high-stakesapplications from certified, trusted software components. Timing estimates madeat design time are routinely within required tolerance with 99.99% confidence or bet-ter.

Critical safety and security properties are formally verified, and one has obtained firmcontrol over the quality of software components developed by suppliers from aroundthe world. These capabilities give a potent differentiator in a increasingly competitiveindustry. Engineering predictability beyond testing is the use of software architec-ture to predictably satisfy the quality requirements of software systems. PACC takesarchitectural predictability to the extreme ranges of rigor and objective confidence,and incorporates architecture design directly into the basic units of software construc-tion. The approach is to develop analytic theories that predict the behavior of entireclasses of systems. In this approach, the emphasis is on confirming the validity oftheories. Once confirmed, one can be sure that all systems satisfying the assump-tions of the theory will have behavior that is predictable in that theory.

Zones of predictability:

PACC divides the world into systems whose behaviors are predictable by analyticmeans and those whose are not, Figure 12, Figure 13. Analytically predictable sys-tems are said to lie within the set, or zone, of predictable assemblies (systems as-sembled from components).

The behavior of assemblies that are in the zone can be determined at design timewith objective confidence. Assemblies that lie outside the zone are not analyticallypredictable. Their behavior can only be observed after they are built.

Figure 12: Component assemblies are “in the zone” if their runtime behavior is analyticallypredictable.

Assemblies may be predictable using any number of analytic theories (timing, secu-rity, safety, fault tolerance, and power consumption) and may therefore lie within anynumber of zones of predictability.

not OK

OK

PACC provable OK

zone

Page 26: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

26

The PACC approach is to ensure that we build only systems that lie within the re-quired zones of predictability. Our focus is on critical qualities that are likely to be ofsignificant business value, such as performance, safety, and security.

Objective confidence Predictions must be trustworthy. Objective confidence,through rigorous empirical and formal validation, is the acid test PACC applies topredictions. This distinguishes PACC from other model-based and generative ap-proaches to software development.

The predicted behaviors of all assemblies have associated measures of confidence.This confidence is the bankable outcome of predictable assembly—leading to shorterdevelopment cycles, decreased development and testing costs, and higher qualitysystems.

Predictability by construction The aim is to build only those systems that havepredictable behavior, rather than to predict the behavior of any systems we build.PACC technology ensures that the assumptions of analytic theories are establishedas invariants during system construction.

So the systems are predictable because the component technology guarantees thatassemblies always stay in their required zones.

Figure 13: Each assembly (system assembled from components) in the zone has a corre-sponding model in that zone’s analytic theory.

Page 27: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

27

Figure 14: PACC Assignment of a statistical confidence label to analytic theories

Trusted components: PACC establishes a foundation for trusted components, onethat goes beyond functional correctness to encompass other “as built” qualities thatcomponents must possess. Analytic theories tell us which qualities are needed tosupport predictability.

Page 28: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

28

Figure 15: Trusted components must provide more insight into their inner workings. Analytictheories require additional quality-specific properties such as task execution time to makepredictions. These quality-specific properties are exposed as analytic interfaces of compo-nents

All analytic theories make assumptions. Some of these assumptions dictate what weneed to know and trust about components. So a performance theory might requirethat we know the maximum non-blocking execution time for all component opera-tions, while a safety theory might require that it’s to possess a state machine for eachcomponent operation.

In these examples, analytic theories require visibility into some aspect of the behavioror implementation of components.

These new visibilities make up the analytic interface of a component. Different ana-lytic theories will, in general, require different analytic interfaces; each such interfacedefines a distinct, analysis-specific view of the component.

To have objective confidence in the predictions of analytic theories, one must alsohave objective confidence in the parameters to these theories components’ analyticinterfaces. PACC therefore establishes an objective, measurable, and predictivefoundation for component trust and certification.

A higher order component technology

The SEI develops a component technology that is parameterized by analytic theo-ries. Filling in these parameters with specific analysis theories, for performance andsecurity for example, results in a prediction-enabled component technology (PECT).Prediction enabling means that systems built using the component technology will beguaranteed by construction to be in the zone of predictability for critical system prop-erties.

Page 29: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

29

Figure 16: To support predictability, a component technology must exhibit the minimal, idealdesign pattern shown above. In this ideal pattern, all interactions among components are ex-posed and use standard connection mechanisms. Additionally, resource management andcoordination policies are defined and enforced by a standard component runtime environment

A strict foundation

A PECT requires a strict and well-defined component technology at its core. Thecomponent technology we use is a result of close examination of the best featuresand patterns found in today’s component technologies. The design pattern differsfrom those patterns in its combination of features and the strictness with which it isenforced. It includes only the features needed to support predictability by construc-tion.

Reasoning frameworks

That is the extension of component technology with reasoning frameworks. The ele-ments of a reasoning framework are an analytic theory, based on a solid foundationsuch as queuing theory, rate monotonic scheduling theory, finite-state automata, ortemporal logic.

Page 30: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

30

8 Ensuring intra- and inter-IMA Communication

Network architectures are explored using network calculus and real-time calculus.The techniques allow by algebraic methods to analyze loads and latencies, a majorstep in validation of IMA and IMA communication. Starting with network calculus,real-time calculus was developed a decade ago. The last years showed that a lot ofreal time system analysis can be derived from real-time calculus.

Meanwhile more efficient algorithms exist for calculating IMA communication, alsoIMA AFDX communication in complex architectures, see Figure 7: AFDX point topoint to communication, to calculate maximum point to point latency under arbitrarybut defined load of the overall system.

Example: Process A on a processor of an IMA sends data to another process insidethe same IMA, this process does calculations, for that is must be scheduled, thisprocess is sending data via AFDX to another processor, on this one is running proc-ess B, This one also has to scheduled to be able to read the data; this latency fromsending from sending from process A to reading of process B, point-to-point, underarbitrary load but under a defined threshold of IMAs and AFDX is to be calculated asguaranteed worst case, to be done for every A-B-connection in the IMA-AFDX net-work, see Figure 20.

Based on the same mathematical basis of network calculus and real-time calculustools are developed allowing dimensioning the system and optimizing the parametersof an IMA / AFDX system being save under worst defined case conditions.

This has to be done under ARINC653 (IMA) / ARINC 664 (AFDX) and AFDX / EREBUS(Extended Robust Ethernet-based Bus).

Page 31: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

FibG

T5

T

Ba

F

D-AV-3.2C

31

igure 17: Tee event spectrum shows different aspects of system behaviour depend-ng on time intervals an calculated from the real-time scheduling analysis tool. It cane done for a single processor or BUS but can also comprise several BUS systems,ateways/Routern/Switches and processors.

he green curve shows the worst case calculation time demands of task B (every0ms a claim of 10ms).

he yellow curve shows the equivalent of task A.

esides that, the remaining camasity of the CPU is shown all 300ms, red curve, ands % load, blue curve.

igure 17: Event spectrum / INCHRON

Page 32: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

FoTTTRn

Figure 18: Pro

D-AV-3.2C

32

igure 18: The process state diagram shows activations, interrupts and blocking byther processes as function of time so depending on the scheduling strategy (FCFS,DMA or fixed Priority).he ecample shows two time triggered prozcesse (Task_TT_1ms andask_TT_5ms), one event based process (Task_CSFT) and a Interrupt-Service-outine (ISR_1ms). Here a fault raises (Activat Limit), for Prozess(Task_TT_1ms) isot terminating in 1 m as it should.

cess state diagram / INCHRON

Page 33: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

Ffpa

Figure 19:

D-AV-3.2C

33

igure 19: The Process states- and influence diagram shows the easy to follow datalow. It shows the flow from a sensor via a FlexRay-Bus to a CPU to an actor. On theath there can be gateways and other CPUs. Loss of data, multiple reading of data,nd age of data are understood.

Prozesszustands- und Wirkkettendiagramm / INCHRON

Page 34: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

34

Figure 20: Causal dependencies, ARINC 664 AFDX example / SYMTA VISION

Page 35: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

FtIt

D-AV-3.2C

35

igure 21: While Figure 18, Figure 19 where simulation based, here we have guaran-eed worst case calculation of the response time of a process. The result is assured.t also calculates the guaranteed best-case. The results can be overestimated, buthey are save worst or best.

Figure 21: Antwortzeiten eines Prozesses / INCHRON

Page 36: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

F

36

igure 22: Process diagram, end to end simulation / SYMTA VISION

Page 37: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

37

Figure 23 shows the coverage of states and transitions (red = not coverd). In thiscase, the missing coverage was triggered by uncomplete connectivity: Stateclustercould be entered but not be leaved again. The system was limited in functionality.The diegram was calculated, not simulated.

Figure 23: State diagram, the coverage of states and transitions

Page 38: Version: 1 - Software Plattform Embedded Systems 2020spes2020.informatik.tu-muenchen.de/results/AV-AP3 D-AV-3.2.C.pdf · D-AV-3.2C 5 1 Positioning and Abstract 1.1 Motivation Das

D-AV-3.2C

-

Figure 24: Graphische Darstellung der von ISG gemessenen Antwortzeiten (Min/Max/Mean), aufgeschlüsselt nach Absen der im Modell. / © BSSE

F -s

igure 25: Graphische Darstellung der von ISG gemessenen Signallaufzeit Sender zu Empfänger (Min/Max/Mean), aufge

chlüsselt nach Absender im Modell. / © BSSE

F -s

igure 26: Graphische Darstellung der von ISG gemessenen Warte

38

chlangengrößen, aufgeschlüsselt nach Prozess. / © BSSE