=Paper=
{{Paper
|id=Vol-2308/aviose2019paper06
|storemode=property
|title=Model-Based Engineering for Avionics: Will Specification and Formal Verification e.g. Based on Broy’s Streams Become Feasible?
|pdfUrl=https://ceur-ws.org/Vol-2308/aviose2019paper06.pdf
|volume=Vol-2308
|authors=Stefan Kriebel,Deni Raco,Bernhard Rumpe,Sebastian Stüber
|dblpUrl=https://dblp.org/rec/conf/se/KriebelRRS19
}}
==Model-Based Engineering for Avionics: Will Specification and Formal Verification e.g. Based on Broy’s Streams Become Feasible?==
https://ceur-ws.org/Vol-2308/aviose2019paper06.pdf
Model-Based Engineering for Avionics: Will
Specification and Formal Verification e.g. Based on
Broy’s Streams Become Feasible?
Stefan Kriebel Deni Raco Bernhard Rumpe Sebastian Stüber
BMW Group Chair of Software Engineering Chair of Software Engineering Chair of Software Engineering
Munich, Germany RWTH Aachen University RWTH Aachen University RWTH Aachen University
Aachen, Germany Aachen, Germany Aachen, Germany
Abstract—Avionics is definitely a safety-critical application Furthermore, refinement of a component in a decomposed
domain. Software complexity is ever increasing together with structure automatically leads to refinement of the composition,
more autonomy as well as increased real-time based interaction which allows to individually develop each component, but also
between airplanes, drones and potentially future air taxis.
This again raises the question, whether developing software to replace variants of implementations along the life cycle of a
the same way as we did the last 30 years is still appropriate, system. High-automation of the proofs, as well as the handling
or in the times of much better formal methods and cheap of feedback loops, unbounded non-determinism, time-sensitive
and powerful computational capabilities, it would be feasible specifications, safety and liveness properties, and refinement
to use clear and model-based specification techniques for an checking are key for an efficient development process.
integrated systems engineering approach and formally verify any
physical and logical implementation of functionality, including The rest of this paper is structured as follows: First, a
the software against that specification. This could be another motivation for the methodology is given. Then, the underlying
important step towards quicker development of highly safety- theory is presented. Next, the tool chain consisting of the
critical systems. frontend DSL, the mathematical backend, and the generator is
illustrated. Finally, the verification of a property of the running
I. I NTRODUCTION example is demonstrated.
In this paper, we demonstrate early results on a small part
II. BACKGROUND
of this systems engineering approach, namely using a user-
friendly architecture description language [1], [2] and proving Designing distributed systems [6], [9] which react in real-
safety-critical properties in the theorem prover Isabelle [3]. time, are dependable and fulfill safety and liveness require-
Because the theory and its underlying methodological concepts ments, is a challenging problem [10]. Formulating require-
are too much to be explained in this short paper, we highlight ments only in natural language is still common in the em-
a small example only, focusing on the demonstration of the bedded industry and the challenging part is to early detect
feasibility of formal verification of complex software. and avoid ambiguity [11] and inconsistencies [6]. In safety-
Therefore, the paper demonstrates the use of the FO- critical systems errors might lead to injury or high costs
CUS framework [4]–[8] for specifying distributed interactive as consequences [12]. For this reason, formal methods, like
systems and verifying safety-critical properties of real-time CSP [13], [14], FOCUS [6], CCS [15], Petri Nets [16], or
critical software such as common in avionics systems. The the π-calculus [17] are used to detect potential sources of
methodology is modular with respect to composition. A user- errors earlier [18], [19]. However, an important property which
friendly architecture description language (ADL) like Mon- makes the methodology of this paper stand out among the
tiArc [1] serves as a developer frontend, allowing a state-based competitors above is that refinement of a component in a
specification of components [8] and enables the definition decomposed structure automatically leads to refinement of the
of the desired safety-critical properties. An appropriate tool composition [7] (thus refinement is fully compositional).
maps the ADL model and its behavior specifications into Avionics have long life cycles and a lot of maintenance
specifications and theorems in the theorem prover Isabelle is needed [20]. Further growth in flying vehicles, passenger
[3]. There, general composition operators exist that compose numbers and cargo is expected. Since the spatial expansion
specifications of the components into a specification of the possibilities of the system infrastructure are limited, the use
overall system. Properties can be specified on a global scale of correct software systems becomes vital [21]. It is thus not
and decomposed as well and proven on atomic components. without reason that the list of considerations for the production
Composition of properties leads to globally correct software. of software for airborne systems named ED-12C/DO-178C has
as its motto: ”the greater the software development rigor, the
fewer errors occur in software design” [22].
AvioSE 2019: 1st Workshop on Avionics Systems and Software Engineering @ SE19, Stuttgart, Germany 87
Safety-critical functionalities in avionics are usually treated
by a complex system management, which deals with fault
detection and redundancy management [23]. The increasing
complexity in avionics is heavily due to [24]:
• the increasing number of features, Fig. 1. Verification tool chain
• the internal complexity of each feature,
• interaction among features,
• better scientific instruments, Components communicate through sending and receiving
• processing large amount of data in real time, messages through directed channels. A stream (a potentially
• thousands of sensors and measurement devices, infinite sequence of messages from an alphabet) [6] represents
• redundant components, ready to automatically configure the communication history of a channel. The semantics [31]
themselves in case of failures. of a (potentially non-deterministic) component is a (set of)
For a stepwise correct design of avionics systems, a model- stream processing functions [8].
based methodology [25], [26] would be beneficial. A modeling Since streams model history, not all functions over streams
ADL offers the architect a way to express the knowledge about model real-life interactions. Only a subset of these func-
a process, and the created models can be translated into other tions fulfilling certain properties are suited to model real-
models or executable code [27]. Most importantly, the models life components. A component cannot take an already emitted
of the software can be tested or verified, independent of the message back. This means that an extension of the input can
hardware. By having testing or verification being performed only lead to an extension of an output. This is known as
parallel to the software model design, before committing to monotonicity [8]. Second, to define liveness properties, one
hardware, the likelihood that design errors are recognized late needs infinite streams to describe full histories. It is however
and potentially bring high costs is reduced. not implementable to look at the complete (infinite) input
Some further reasons for the usefulness of testing or veri- stream to emit an output message (which of course occurs
fying the software models are [24]: after a finite time). Enforcing this means restricting the set of
• by verifying early in the life cycle before hardware is
functions to the so-called continuous ones [4]. In addition to
available, one reduces the number of needed tests on the restraining from reacting to infinity, continuous functions also
physical system, guarantee the existence and the inductive computation of least
• software models can enable one to have access to sub-
fixed points, which is necessary to give meaning to feedback
modules and test those separately, whereas in hardware loops [6], [8], [32].
this might be in some cases physically not possible, All above mentioned domain-theoretical concepts has been
• even if sometimes accessing hardware sub-modules might
formalized in the theorem prover Isabelle/HOLCF (HOL
be possible, it might mean causing damage to it, stands for higher-order logic, CF stands for computable func-
• testing fault protection behaviors might be highly costly
tions) in [33], [34] and [35] independently formalized parts
and damaging. of FOCUS in Isabelle/HOL (without domain-theory). [36]–
Testing components, however, on all combinations of inputs [41] were some first results in formalizing streams in the
and states (represented by the variable values at a certain point theorem prover Isabelle with domain-theoretical concepts, and
in time) might be not feasible. In addition, when comparing constitute the foundation of this paper. On the other hand,
testing strategies from the literature, it is usually hard to show the tool-chain named AutoFOCUS [42] has had early results
that one testing strategy would always detect more faults than in using the HOL-formalization of FOCUS. A further related
another one [28]. work to formalize model component networks is the Ptolemy
In this paper a methodology for specifying and verifying Project [9], [43] where the authors create a framework for
distributed interactive systems is demonstrated and applied on actor-oriented design. Also, an approach to verify AADL-
an example. models is presented in [44].
For simple event-based communication, an untimed stream
III. U NDERLYING T HEORY approach is sufficiently expressive to model an interactive
The methodology presented in this paper builds on the system. In real-time systems, however, a timed model is
mathematical underpinning FOCUS [6] and is implemented much more appropriate. This allows software to react on
as a tool chain depicted in Fig. 1, being particularly suited for absence of messages and signals. A formal specification of
usage in safety-critical systems such as avionics. The frontend such a software component therefore does not only incorporate
of the tool chain MontiArc [1] (created with MontiCore [29], reactive behavior, but also timing specification on both sides:
[30]) is a developer-friendly domain-specific language for the along with a component’s reaction, it is also considered how
specification of component interfaces, their behavior and their long the neighbor systems, sensors etc. have time to respond.
composition. A MontiArc model is transformed by a code One mathematically simple and powerful way to model time is
generator into an Isabelle automaton specification, and then to extend the set of sent messages with a virtual element called
this (potentially non-deterministic) automaton is mapped to tick and enforce infinitely many ticks in each infinite behavior
its semantics, namely a (set of) stream processing functions. observation. Two consecutive ticks describe an equidistant
AvioSE 2019: 1st Workshop on Avionics Systems and Software Engineering @ SE19, Stuttgart, Germany 88
time interval with only finitely many occurring messages. In inserting substates.
certain circumstances this observation may be reduced to at The most important property which makes this methodology
most one or even exactly one message per time interval. Focus stand out among competitors (like CSP [13] [14], CCS [15],
is capable of handling all these variants even in combination. Petri Nets [16], or the π-calculus [17]) is that refinement of
Focus can also look at different time scales [45], [46] allowing component specifications is semantically reflected by the con-
the developer to select the right time abstraction for each cept of set inclusion between function sets and that refinement
component. of a component in a decomposed structure automatically leads
As said, specifications of component behavior are math- to refinement of the composition [7]. That means, refinement
ematically formalized as a set of functions mapping timed is fully compositional. This property is a major reason why
input streams to timed output streams. To model correct this proposed methodology is well-suited to specify larger
behavior (i.e. not looking in to the future), some restrictions, and complex distributed systems, because it allows to scale
such as weak-causality or even embodying some delay in a specification from atomic components to large systems,
form of strong-causality e.g. to avoid the Brock-Ackermann such as airplanes. One can specify a system, decompose the
anomaly [6], [47] in feedback compositions. The concept specification, refine the individual sub-systems until an im-
of monotonicity, continuity and causality are often generally plementation is reached, and then have the guarantee that the
referred to as realizability or interactive computability [48], composition of the implementations is correct by construction.
the equivalent concept to computability of partial functions Furthermore, a component library with popular components
carried over to interactive systems. (NOT, AND, OR, NOR, XOR, ADD, Delay, variants of
To support system decomposition, operators for sequential, a transport medium, counters, timers, etc.) was created to
parallel and feedback composition are encoded in Isabelle, as support specifications. For example the transport medium-
well as a general composition operator [7], [49]. A high-level components have an abstract non-deterministic specification
API is provided in this work to hide fixed-point theory from (the set of implementations describing their possible behaviors
the user. is even uncountable) and also a number of refined behaviors,
One of the strengths of the methodology of this work is that resembling special characteristics such as liveness properties.
by using a variant of non-deterministic and thus underspecified In essence, without going deeper in details in this short
state machines with input/output [8] to define the components paper, the formalization of refinement checking of (potentially
behavior, the system is by construction realizable [6], [50]. unbounded) non-deterministic specifications consisted in the
Those state machines receive their semantics as sets of stream encoding in Isabelle of the corresponding refinement calculus
processing functions [8] and are thus fully integrated into the from [8]. The correctness of the refinement steps is also
refinement and composition framework that FOCUS provides used to show that the system doesn’t gain new, potentially
within Isabelle. These realizable stream processing functions undesired, behaviors and the properties of the initial system
are an abstraction to the automata with input/output from [7], are automatically derived for the refined system as well (the
[8] in the same way that partial functions are an abstraction user is thus relieved from the necessity to prove these again for
to the Turing machines. the new system). Along with the specification, a set of useful
One important particularity of this methodology is that the theorems and their proofs are generated for each component,
composition of realizable functions is realizable as well [7], which increases the automation of the proof of the desired
[49]. So a realizable composed system can be hierarchically system property.
decomposed into a collection of realizable components, each Finally, abstract theorems are provided to enable an auto-
represented by a (set of) stream processing functions. This way matic checking of safety and liveness properties. We under-
a complex architecture can be built in a fully compositional stand informally by
way.
• safety: properties that can be falsified by finite streams.
As already mentioned, sets of functions are used to give
• liveness: properties that can be falsified only by infinite
specifications a meaning allowing multiple behaviors, either
streams.
due to potential non-determinism of the components, or due
to insufficient information during development. The methodology is demonstrated in this paper on a feature
Refinement is used to make underspecified components interaction scenario of a light control, which is actually
specifications more precise along the development process. taken from the automotive domain, but we expect that the
Underspecified behavior can be refined towards an implemen- avionics domain could be very similar. The (small part of the)
tation. Refinement of non-deterministic automata is semanti- system and a desired property are defined through an explicit
cally represented by set inclusion of sets of stream processing specification and the desired safety-critical property is proven
functions [7], [8]. A number of important refinement tech- at the push of a button. The full-automation is the result of:
niques, such as transition refinement and state decomposition • the encoding of thousands of general, case study inde-
are formalized in order to automate the checking of refinement pendent theorems for interactive components and their
correctness. Transition refinement means that by removing one composition in Isabelle,
of a set of alternative transitions, the set of behaviors becomes • a library of common generic reusable components to-
more precise. State refinement allows e.g. splitting states by gether with proven properties over these,
AvioSE 2019: 1st Workshop on Avionics Systems and Software Engineering @ SE19, Stuttgart, Germany 89
• the development of the corresponding code generator for Chosen safety-critical property informally: The alarm
all mathematical structures introduced above. system always has highest priority. So if the alarm is activated,
This case study demonstrates the correct encoding and the interior light will turn on, no matter how both the door
usage of a general composition operator, dealing in particular status and the light switch behave.
successfully with feedback cycles by generating appropriately V. M ONTI A RC IN I SABELLE
a delay, as well as handling time-sensitive specifications.
An untimed stream is a (potentially infinite) sequence of
IV. T HE DEVELOPER - FRIENDLY ADL M ONTI A RC messages over a carrier alphabet M. M ω denotes all streams
and is the union of M ∗ the finite ones and M ∞ the infinite
A user friendly domain specific ADL is presented, to ones. To construct streams, the constructor ” : ” with signature
enforce the specification of realizable-per-construction compo- M ⇒ M ω ⇒ M ω is defined. The operator _ denotes the
nents [1]. It enables the high-level specification of composed concatenation of two streams [6]. Based on the construction
systems, as in Fig. 2. A running example dealing with com- operator on streams, we can define an ordering v on the set
municating controllers in vehicles is used to ilustrate this. of streams. The prefix ordering [8] on streams v is defined
such that the following holds:
∀x, y ∈ M ω . x v y ⇔ ∃s ∈ M ω . x _ s = y
Please note that the prefix order defines a partial order on
streams [8] and that M ω completes M ∗ to a complete partial
order [34] with respect to prefixing.
To specify time-sensitive behavior, timed streams are used
(in our case study the so-called time-synchronous streams
variant). For this, the message alphabet is extended by a
dummy element ∼ (read eps). In this interpretation we assume
a discrete global clock and each element of the stream is either
a message arriving during each (equidistant) time frame, or an
∼ (interpreted here as ”no message has arrived”, having also
the length of one time frame).
Fig. 2. Communicating controllers in vehicles Streams have been encoded in the interactive proof assistant
Isabelle [51]. The proofs, data structures as well as functions
In a black box view a component is defined by its input are there formalized in so-called theory files, which have the
and output channels. Each channel is identified by a name and following structure:
the data type of the messages allowed to flow in it. Generic
t h e o r y ExampleTheory
data types are supported in order to facilitate reuse. Composed
i m p o r t s Main
systems are defined by importing the subcomponents and
begin
connecting the channels. Output channels of a component can
( * d e f i n i t i o n s and lemmas * )
be connected to input channels of the same or of other com-
end
ponents. It is allowed to use the same subcomponents multiple
times. Generic data types can be instantiated multiple times. The implementation in the theorem prover Isabelle of the
Additional information can also be added to the model. For data type stream is, apart from some technical domain-
example invariants of components, or whether the component theoretical details [37], similar to lazy lists of (say) Haskell.
is deterministic or not.
domain ’ a s t r e a m =
The depicted controller InteriorLightArbiter controls the in-
lsconc ” ’ a” ( lazy ” ’ a stream ”)
terior light of a car. The description of the formal specification
of interfaces, behavior and composition will be introduced The keyword domain [34] generates the prefix ordering
later. As can be seen, this system produces its output based and a bottom element (the empty stream). The constructor
on the light switch, the car’s doors and the alarm system. lsconc appends an element to the rest of the stream.
Depending on these inputs, it emits a command to turn the Fig. 3 gives an overview of our theories, such as Stream
interior light on or off. For example it evaluates the light Bundles (SB), stream processing functions (SPF), and sets of
switch status by simply forwarding its status. The interior light functions denoted as stream processing specifications (SPS).
is also switched on if the door is opened, and goes out a Foundamental theories such as LNat (lazy natural numbers,
short while after the door has been closed again. A closed where the set of naturals is extended with an element denoting
door only changes the light status if the door is closed since 5 infinity), or SetPcpo (sets are enhanced with a subset-order)
seconds. If the alarm system is active, the interior light blinks. are needed as well. Theory imports are represented as arrows
As long as its incoming signal value is on, the Flasher outputs in the Figure. These mathematical structures will be briefly
alternatingly on and off values. described later.
AvioSE 2019: 1st Workshop on Avionics Systems and Software Engineering @ SE19, Stuttgart, Germany 90
the flexibility in defining general composition over arbitrary
number of channels).
A deterministic component is modeled by a stream(bundle)
processing function (the type denoted as SPF), which is then
a continuous function mapping stream bundles to stream
bundles. The semantics of a non-deterministic automaton is a
set of stream processing functions (the type denoted as SPS).
VII. S TATE - BASED MODELING
As mentioned, state-based modeling is used to enforce the
specification of realizable-per-construction components. We
demonstrate an example by specifying the behavior of the
DoorDelay component in Fig. 4:
Fig. 3. Structure of the theories
The extension to time-synchronous streams is also done
similarly as one would extend a data type in Haskell: given
the type stream over a parametric type-variable 0 a, and a
constructor for messages M sg, one can then define:
datatype 0 a tsyn = Msg 0 a | ∼
Fig. 4. Behavior of DoorDelay as Automata
An instance of a stream of natural numbers over tsyn would
then be e.g: Msg 1, ∼, Msg 2, ∼, ∼,.... This is read as: the first
This figure is a graphical representation of the behavior
time slot sees the message 1 arriving; in the second time slot
represented by the following MontiArc textual description.
no message arrives; in the third one the message 2 arrives,
The time model in the textual description is set to time-
and after that no more messages arrive. The granularity of
synchronous (sync). Then the interface of the component
each time interval can be set depending on the case study
(ports and input/output channels) is defined. A variable delay
(say ”minutes”, if we are modeling bus arrival times, or say
is used to represent the states. Finally the behavior description
”milliseconds”, if we are modeling communication inside a
is given by listing the transitions. Transitions are enhanced by
computer processor.)
input/output.
In our light controller the elements of the streams flowing
in the channels are from the carrier set B ∪ {∼}. component DoorDelay {
VI. S TREAM BUNDLES AND S TREAM P ROCESSING timing sync ;
F UNCTIONS
To facilitate composition, we enhance our modeling of com- port
ponent networks by naming channels and defining composition in boolean i ,
operators which connect channels of the same name and type. out boolean o ;
The user can then define the type of a channel via a function
which for each channel returns a set of allowed messages, i n t delay ;
i.e., the domain of the channel type. To model the input (or
output) streams of a component, we work with an isomorphic a u t o m a t o n DoorDelay {
transformation of the tuples of streams (instead of just working state S;
on tuples): namely with mappings from channel names to i n i t i a l S / { delay =0};
streams. Such a mapping is then called Stream Bundle [8]
if the messages of the streams mapped to the channels are S [ ! i && d e l a y >0] /
allowed to flow on it. Thus, we can compose components and { d e l a y = d e l a y −1 , o= t r u e } ;
define generalized composition operators [7] connecting same- S [ ! i && d e l a y ==0] / { o= f a l s e } ;
named/same-typed channels without worrying about setting S [ i == n u l l && d e l a y >0] /
preconditions for the interface compatibility. In the case of { d e l a y = d e l a y −1 , o= t r u e } ;
(say) an addition component, the encoding in Isabelle of the S [ i == n u l l && d e l a y ==0] / {o= f a l s e } ;
interface of the input would be the structure of the form S [ i ] / { d e l a y =5 , o= t r u e } ;
[channel1 7→ stream1 , channel2 7→ stream2 ] (instead of }
the intuitive tuple (stream1 , stream2 ), which does not offer }
AvioSE 2019: 1st Workshop on Avionics Systems and Software Engineering @ SE19, Stuttgart, Germany 91
As a contrast to state-based specifications, a specification above mentioned special operators as shown in Fig. 6, where
such as DoorDelay[a : b : c : d : e : xs] = f (a, b, c, d, e, xs) c1 ...c8 denote here the channel names.The general operator is
for some function f , messages a, b, c, d, e, and sequence of equally powerfull to the combination of all special operators.
messages xs might lead to non-realizable behavior, since one The generated stream processing functions are automatically
can make use of (say) b in the first output time slot before it connected by this operator. The proof of commutativity and
has arrived as input. associativity [6] of this operator is also encoded in Isabelle.
The behavior of the AND, OR, and NOT components is a This means that the order of composition of a list of compo-
straightforward lifting from booleans to streams of booleans nents does not matter.
and the boolean values have priority over ∼.
The behavior of a MontiArc component is specified as
automata with input/output [8]. Automata with input/output
consist of states and transitions. The states of the automaton
are used to save information about the current state of the
computation. In addition to states java-variables can be used
in MontiArc.
Transitions help define the behavior of a component. A
transition describes the output and new state of a component.
Non-determinism can be modeled by multiple transitions or
by a single transition with a set as result.
Each automata is translated in a final step into (sets of)
stream processing functions, which constitute their semantics
[8]. The Isabelle theory of stream processing functions is rich
with theorems, which increase the automation of the proofs.
VIII. C OMPOSITION AND FEEDBACK LOOPS
To decompose and then re-compose components in a de-
velopment life cycle, special composition operators of Fig. 5
were encoded using the notations as described in [7]
Fig. 6. General Composition Operator
IX. N ON - DETERMINISTIC SPECIFICATIONS
Fig. 5. Special Composition Operators Our mathematical model is expressive enough to model
interesting aspects of software development such as underspec-
Serial composition in a) is quite straightforwardly overtaken ification and refinement as well. From a user’s point of view, it
from function composition in mathematics, and parallel com- is not distinguishable, whether a system is underspecified (fur-
position in b) creates a new component with an extended ther refinement steps during the development process can make
interface. specifications more precise), or it makes non-deterministic
The µ-operator for feedback in c), such as the one occurring decisions on runtime. In the introduction of this paper, we
in the Flasher-Component, is defined as follows: for streams already mentioned that components may be under-specified
x, y, z we have (z, y) = (µf ).x, if (z, y) is the least fixed or non-deterministic. Thus, a single deterministic SPF is not
point of the equation (z, y) = f (x, y). sufficient to describe all possible component behaviors, and
Streams flowing on feedback loops are defined as least fixed instead a set of stream processing function must be used to
points of the corresponding equations [5]. Monotonicity is model the component behavior properly [49]. Nevertheless,
neccesary for least fixed points to be unique. the input and output channels of components are fixed, thus
A general composition operator f ⊗ g was encoded [5], all stream processing functions in such a set must have the
[7], [39] as well, covering all possible combinations of the same input and output channels.
AvioSE 2019: 1st Workshop on Avionics Systems and Software Engineering @ SE19, Stuttgart, Germany 92
X. C ODE GENERATOR FROM M ONTI A RC TO I SABELLE is proven to be reducible to a parallel composition between
To verify the properties of user-defined component systems, these. As a next step, the composition Flasher ⊗ OR is shown
they are automatically transformed to specifications and theo- to be reducible to a serial composition. These reductions are
rems in Isabelle. recognized automatically by investigating the shared channels
The equivalence of the user-specification and the generated between components. The large amount of encoded theorems
Isabelle-specification is imperative for any logical reasoning. A about the special operators, as well as the extension of the
complex generation process could lead to different semantics. code generator with common component-specific properties,
To reduce complexity of the transformation, MontiArc-ADL take care of the rest, making this property proven at the push
and Isabelle-Specification are using similar concepts. of a button.
An automata [8] is first transformed from the MontiArc
model to an automata in Isabelle. The abstract syntax of XII. C ONCLUSION
automata is encoded in Isabelle as well. In a second step the
In this paper, we have seen that there is an appropriate
automata is mapped to its semantics, a set of stream-processing
theory, namely Broy’s streams [6], which is able to describe
functions [8]. The second step is entirely within Isabelle and
behavior of real-time capable distributed and complex software
its correctness is proven.
in a hierarchically decomposable form. Furthermore, along the
A composed specification is realized through the general
development process refinement of underspecified component
composition operator [39]. Since the general composition
behavior is possible and is fully compatible with the compo-
operator can only connect channels with the same name,
sition operators. That means decomposed subcomponents can
internal channels are used. These internal channels are not
be individually implemented and desired properties proven on
visible in the public interface of the component.
local components thus that the overall composed system is
XI. V ERIFICATION OF P ROPERTIES then correct by construction.
MontiArc invariants are mapped to Isabelle lemmata. Sim- Correct by construction means that there is no complicated
ple properties can be proven automatically, whereas more integration phase with lots of errors only identified late in
complex properties might require user interaction. To simplify the development process. Instead a rather agile development
any manual proof, additional lemmata are generated. One process could become possible: It has an always integrated
can specify his desired (potentially safety-critical) property composed system with individual subsystems hierarchically
in MontiArc. The framework is extended sufficiently with decomposed and individually refined along the development.
abstract theorems, such that most simple properties will be The encoding of Broy’s Stream Theory in Isabelle and the
checked on the push of the button. This is also the case for available comfortable modeling techniques, such as an ADL as
the chosen property of this work, thus showing promising well as state machines are an important step towards a rigorous
results about the feasibility of the approach. It is shown that development process based on model-based specifications and
the alarm status has priority over other inputs and it guarantees formal verification.
the turning on of the light, no matter how both the door status However, there are still a lot of steps to do. (1) The
and the light switch behave. integration of modeling techniques as developers frontend
Let snth n denote the time slot of a message in a stream needs to be tighter and potentially also handle other forms
for some natural n, AlarmStatus the input stream of of modern specification languages. (2) The library of avail-
the light controller, and OnOf f Cmd the output stream of able predefined components and their specifications must be
the light controller. The theorem is then formulated as follows: intensively extended. (3) The proof assistant system needs to
be robust and as automatic as possible in any kind of potential
theorem: ∀ n ∈ N : snth n AlarmStatus = True ⇒ situations. Ideally the proof assistant is so highly automated,
((snth n OnOffCmd = True) ∨ (snth (n − 1) OnOffCmd = that ordinary software developers do not explicitly have to
True)) cope with proving activities at all, but can concentrate on spec-
< proof > ifying behaviors on different levels of abstraction, while the
underlying proof assistant tells the developers automatically,
The proof is automatically generated. whether their development steps have been correct. This would
Here is a proof sketch. First one checks the correctness lead to a continuous verification system quite like the currently
of the single components. The Flasher is trickier, since it already existing continuous integration environments [52] for
contains a feedback loop. It was first shown, that the output compilation, generation and testing.
stream of the Flasher corresponds to the certain desired least Of course, in practice a combination of all these techniques
fixed point. The proof of correctness for components with is desired. Based on our experiences, we believe that formal
feedback loops and for those with a state(such as DoorDelay) verification should actually be a strong tool in the toolbox of
takes usually the majority of effort to automatize. The correct a mature Software Engineering discipline. However, Software
behavior of the OR-component is also proven. The relation Engineering is still not mature and only future research and
between the AND-Component and the Flasher is mapped to a industrial applications can show whether and how formal
general composition AND ⊗ Flasher. Then this composition verification tools will be part of our future toolbox.
AvioSE 2019: 1st Workshop on Avionics Systems and Software Engineering @ SE19, Stuttgart, Germany 93
R EFERENCES [27] Stephan Rudolph. Know-How Reuse in the Conceptual Design Phase
of Complex Engineering Products, pages 23–39. 01 2007.
[1] Arne Haber, Jan Oliver Ringert, and Bernhard Rumpe. MontiArc -
[28] Ilinca Ciupa, Alexander Pretschner, Manuel Oriol, Andreas Leitner, and
Architectural modeling of interactive distributed and cyber-physical
Bertrand Meyer. On the number and nature of faults found by random
systems, volume 2012,3 of Technical report / Department of Computer
testing. Softw. Test., Verif. Reliab., 21:3–28, 2011.
Science, RWTH Aachen. RWTH and Technische Informationsbiblio-
[29] Holger Krahn, Bernhard Rumpe, and Steven Völkel. Monticore: a
thek u. Universitätsbibliothek and Niedersächische Staats- und Univer-
framework for compositional development of domain specific languages.
sitätsbibliothek, Aachen and Hannover and Göttingen, 2012.
CoRR, abs/1409.2367, 2014.
[2] Aerospace SAE. Architecture analysis and design language. 2004. [30] Katrin Hölldobler and Bernhard Rumpe. MontiCore 5 Language
[3] Tobias Nipkow Lawrence C Paulson and Markus Wenzel. A proof Workbench Edition 2017. Aachener Informatik-Berichte, Software
assistant for higher-order logic, 2013. Engineering, Band 32. Shaker Verlag, December 2017.
[4] Manfred Broy, Frank Dederichs, Claus Dendorfer, Max Fuchs, [31] David Harel and Bernhard Rumpe. Meaningful modeling: what’s the
Thomas F. Gritzner, and Rainer Weber. The design of distributed semantics of” semantics”? Computer, 37(10):64–72, 2004.
systems: An Introduction to FOCUS. Citeseer, 1992. [32] Stephen Cole Kleene. Introduction to metamathematics, volume v. 1 of
[5] Manfred Broy. Functional specification of time-sensitive communicating Bibliotheca mathematica. A series of monographs on pure and applied
systems. ACM Transactions on Software Engineering and Methodology, mathematics. Wolters-Noordhoff Pub, Groningen, 1952.
2(1):1–46, 1993. [33] Franz Regensburger. HOLCF: Eine konservative Erweiterung von HOL
[6] Manfred Broy and Ketil Stølen. Specification and development of inter- um LCF. na, 1994.
active systems: Focus on streams, interfaces, and Refinement. Springer, [34] Brian Charles Huffman. HOLCF ’11: A definitional domain theory for
New York, 2001. verifying functional programs. Portland State University, [Portland, Or.],
[7] Manfred Broy and Bernhard Rumpe. Modulare hierarchische 2012.
Modellierung als Grundlage der Software- und Systementwicklung. [35] Maria Spichkova. Specification and Seamless Verification of Embedded
Informatik-Spektrum, 30(1):3–18, 2007. Real-Time Systems: FOCUS on Isabelle. VDM Verlag Dr. Müller
[8] Bernhard Rumpe. Formale Methodik des Entwurfs verteilter objektori- Aktiengesellschaft & Co. KG, Saarbrücken, 2008.
entierter Systeme. Doktorarbeit, Technische Universität München, 1996. [36] Borislav Gajanovic and Bernhard Rumpe. Isabelle/hol-umsetzung strom-
[9] Edward A. Lee. Fundamental limits of cyber-physical systems modeling. basierter definitionen zur verifikation von verteilten, asynchron kommu-
ACM Transactions on Cyber-Physical Systems, 1(1), 11 2016. nizierenden systemen. Technical report, Technical Report Informatik-
[10] Chih-Hong Cheng, Michael Geisinger, Harald Ruess, Christian Buckl, Bericht 2006-03, Braunschweig University of Technology, 2006.
and Alois Knoll. Mgsyn: Automatic synthesis for industrial automation. [37] Borislav Gajanovic and Bernhard Rumpe. Alice: An advanced logic for
volume 7358, pages 658–664, 07 2012. interactive component engineering. CoRR, abs/1410.4381, 2007.
[11] Grischa Liebel, Anthony Anjorin, Eric Knauss, Florian Lorber, and [38] Sebastian Stüber. Eine domain-theoretische Formalisierung von
Matthias Tichy. Modelling behavioural requirements and alignment with strombündel-verarbeitenden Funktionen in Isabelle. Bachelorarbeit,
verification in the embedded industry. pages 427–434, 01 2017. RWTH Aachen, 2016.
[12] Rashidah Kasauli, Eric Knauss, Benjamin Kanagwa, Agneta Nilsson, [39] Jens Christoph Bürger. Modular Hierarchical Modelling and Verification
and Gul Calikli. Safety-critical systems and agile development: A of Systems using General Composition Operators. Bachelorarbeit,
mapping study. pages 470–477, 08 2018. RWTH Aachen, 2017.
[13] C.A.R Hoare. Communicating sequential processes. [40] Marc Wiartalla. Compositional Modelling and Verification of Distributed
[14] Robert Heim, Pedram Mir Seyed Nazari, Jan Oliver Ringert, Bernhard Systems with special Composition Operators. 2017.
Rumpe, and Andreas Wortmann. Modeling robot and world interfaces [41] Mathias Pfeiffer. A Code Generator for Modeling Underspecification of
for reusable tasks. In Intelligent Robots and Systems (IROS), 2015 State-based Network Components. Masterarbeit, RWTH Aachen, 2018.
IEEE/RSJ International Conference on, pages 1793–1798. IEEE, 2015. [42] Sebastian Voss and Sergey Zverlov. Design space exploration in
[15] Robin Milner. Communication and concurrency, volume 84. Prentice autofocus3 - an overview. In Vladimı́r Mařı́k, JoseL. Martinez Lastra,
hall New York etc., 1989. and Petr Skobelev, editors, IFIP First International Workshop on Design
[16] Wolfgang Reisig. Petri nets: an introduction, volume 4. Springer Science Space Exploration of Cyber-Physical Systems. Springer, 2014.
& Business Media, 2012. [43] Edward A. Lee. Computing needs time. Communications of the ACM,
[17] Robin Milner. Communicating and mobile systems: the pi calculus. 52(5):70–79, May 2009.
Cambridge university press, 1999. [44] Bernard Berthomieu, J.-P. Bodeveix, Silvano Dal Zilio, Pierre Dissaux,
[18] Anthony Hall. Seven myths of formal methods, 1990. Mamoun Filali, Pierre Gaufillet, Steve Heim, and François Vernadat.
[19] Shahar Maoz, Nitzan Pomerantz, Jan Oliver Ringert, and Rafi Shalom. Formal verification of aadl models with fiacre and tina. 2010.
Why is my component and connector views specification unsatisfiable? [45] Manfred Broy. (inter-)action refinement: The easy way, 1993.
2017. [46] Manfred Broy. Refinement of time. In ARTS, 1997.
[20] Andreas H Schweiger. Applying software patterns to requirements [47] J Dean Brock and William B. Ackerman. Scenarios: A model of non-
engineering for avionics systems. 2013 IEEE International Systems determinate computation. pages 252–259, 01 1981.
Conference (SysCon), pages 25–30, 2013. [48] Manfred Broy. Computability and realizability for interactive computa-
[21] Ralf God and Ulrike Wittke. Cyber-physical aviation. pages 4–6, 2016. tions. Inf. Comput., 241(C):277–301, April 2015.
[22] Grischa Liebel, Anthony Anjorin, Eric Knauss, Florian Lorber, and [49] Jan Oliver Ringert and Bernhard Rumpe. A Little Synopsis on Streams,
Matthias Tichy. Modelling behavioural requirements and alignment with Stream Processing Functions, and State-Based Stream Processing. Int.
verification in the embedded industry. 01 2018. J. Software and Informatics, 5(1-2):29–53, 2011.
[23] Darbaz Darwesh, Bjoern Annighoefer, and Reinhard Reichel. A demon- [50] Manfred Broy. Computability and realizability for interactive computa-
strator for the verification of the selective integration of the flexible tions. Information and Computation, 241, 01 2015.
platform approach into integrated modular avionics. 09 2018. [51] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Is-
[24] Mohammed Khan, Michael Sievers, and Shaun Standley. Model-based abelle/HOL: A proof assistant for Higher-Order Logic, volume 2283
verification and validation of spacecraft avionics. 06 2012. of Lecture notes in artificial intelligence. Springer, Berlin [etc.], 2002.
[25] Bernhard Rumpe. Modellierung mit UML. 01 2004. [52] John Ferguson Smart. Jenkins: The Definitive Guide. O’Reilly Media,
[26] Bernhard Rumpe. Agile Modellierung mit UML: Codegenerierung, Inc., 2011.
Testfälle, Refactoring. 01 2012.
AvioSE 2019: 1st Workshop on Avionics Systems and Software Engineering @ SE19, Stuttgart, Germany 94