=Paper=
{{Paper
|id=Vol-2581/aviose2020paper3
|storemode=property
|title=An Approach for Logic-based Knowledge Representation and Automated Reasoning over Underspecification and Refinement in Safety-Critical Cyber-Physical Systems
|pdfUrl=https://ceur-ws.org/Vol-2581/aviose2020paper3.pdf
|volume=Vol-2581
|authors=Hendrik Kausch,Mathias Pfeiffer,Deni Raco,Bernhard Rumpe
|dblpUrl=https://dblp.org/rec/conf/se/KauschPRR20
}}
==An Approach for Logic-based Knowledge Representation and Automated Reasoning over Underspecification and Refinement in Safety-Critical Cyber-Physical Systems==
https://ceur-ws.org/Vol-2581/aviose2020paper3.pdf
An Approach for Logic-based Knowledge
Representation and Automated Reasoning over
Underspecification and Refinement in
Safety-Critical Cyber-Physical Systems
Hendrik Kausch Mathias Pfeiffer Deni Raco Bernhard Rumpe
RWTH Aachen University RWTH Aachen University RWTH Aachen University RWTH Aachen University
Aachen, Germany Aachen, Germany Aachen, Germany Aachen, Germany
Abstract—In this paper the extension of an intelligent compo- exponentially with the size of the (state space of the) system
sitional verification framework for cyber-physical systems is pre- (while e.g. in theorem proving this growth is rather linear [5]).
sented and the capabilities of accompanying underspecification-
refinement steps by verification are demonstrated on a represen- Meanwhile, artificial intelligence fields such as logic and
tative example of a flight guidance system. Formal knowledge knowledge representation have also been applied successfully
representation using higher-order logic and intelligent reason- in software engineering. When representing knowledge by
ing is shown to be applied to software engineering problems logic, theorem proving is then reduced to intelligent rea-
to perform correctness proofs, execute symbolic tests or find soning. So by creating a knowledge base for safety-critical
counterexamples. The theorem prover Isabelle is a mature and
fundamental tool, which allows to represent knowledge as a systems, automatic reasoning becomes possible by reducing
collection of definitions and theorems and reason about systems. verification into applying AI techniques such as metaheuristic
To increase the usability, an architecture description language (proof-) search techniques. Same holds for error detection;
(ADL) coupled with a code generator from the ADL to Isabelle a counterexample-finder takes as input a system model, (the
is used. These and the rapid increase of computation capabilities negation of) a property, and error detection is reduced into a
suggest that a prominent application for reducing certification
costs of critical systems such as intelligent flight control systems search problem (and in case of an error the trace-path of this
or assistance systems for air or road traffic management is not search is returned as a malicious input). In a time of increasing
far in the future. computational power, these techniques open up possibilities to
maintain manageable certification costs.
I. I NTRODUCTION Common ADLs used for model-based development avionics
are AADL [6], SysML [7], Simulink [8] etc. SCADE [9]
The complexity of safety-critical systems is increasing in the (based on the dataflow language Lustre [10]) is used by Airbus
avionics and other fields and new technologies like unmanned [4] coupled with a model checker. In comparison, our ADL
flying vehicles are rapidly introduced into the market. These presented in this paper is extended to be able to handle
bring new challenges to certification processes. While trying not only SCADE-like time-sensitive deterministic systems
to maintain high system reliability, the scalability of traditional (such as our previous automotive case study in [11]), but
quality assurance methods such as testing and reviewing is not also (higher-level predicative-oriented and lower-level state-
ideal and causes considerable amount of costs [1]. oriented) underspecification and refinement.
If requirements were to be specified in a formal way, one
For the incorporation of analysis tools in their life-cycle
could reason about them and thereby replace or complement
processes, companies such as Airbus and Dassault Avionics
many tests (please see also the conclusion for a more detailed
have identified a number of requirements [9], [12]:
discussion). Abstract Interpretation [2], [3] is a static analysis
technique which has been applied in avionics. It does acts • Soundness
rather on code-level (in contrast to the approach of this paper, • Ability to be integrated into the certification standards
which handles requirements on all abstraction levels.) While conforming process
having good automation, Abstract Interpretation is usually • Cost Savings
targeted on very specific artifacts and usually requires some • Deliver correctness by construction
manual expertise to discharge false positives. Model Checking • Scalability: Compositional Verification
[4] also has been applied to small and middle sized systems. • Expressivity of Specification Language
But it does suffer from the well-known state-explosive problem • Timing aspects and underspecification refinement
when trying to handle larger systems. While hardware is • Usability by normal software engineers on normal ma-
better handled, the complexity of verifying software increases chines
Copyright © 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
The Chair for Software Engineering at the RWTH Aachen System
A
University has been conducting research for many years us- Requirements
ing its language workbench MontiCore [13] for developing E -Verifiability
domain-specific languages (DSLs) and also performing model -Verifiability -Accuracy and
-Accuracy and Consistency
transformations. A model transformation could be for example consistency I -Compliance
-Traceability
a refinement [14] of an underspecified model into a more
High-Level F High-Level
specified one in the same modeling language, or a code Requirements B Requirements‘
generator mapping a model from a domain-specific front end
-Verifiability -Compliance -Verifiability -Compliance -Verifiability
language into an equivalent model in an analysis tool (e.g. a -Accuracy and -Traceability -Accuracy and -Traceability -Accuracy and
consistency Consistency
model checker or a theorem prover). H consistency D
In principle, for any DSL one can create a knowledge base
Software Low-Level G Software Low-Level
and reason about it in a logic language. In this paper this is Architecture Requirements Architecture Requirements‘
demonstrated on the example of an architecture description
language (ADL) for cyber-physical systems (called MontiArc -Compliance
C
[11], [15]) coupled with a code generator from the ADL into K -Compliance
-Traceability
the knowledge base (here theorems in Isabelle). The added -Verifiability
-Accuracy and
value demonstrated in this paper is accompanying step-wise re- consistency Source
J Code
finements during the design-lifecycle of safety-critical systems
by verification to reduce certification costs. The knowledge
base consists in the encoding of generic dataflow-oriented data
structures, functions and theorems for reasoning in the theorem Fig. 1. Certification Activities (Letters = Sections in Chapter 2). The denoted
activities are shown to be handled by our methodology and thus save a lot of
prover Isabelle [16]. The semantical [17] underpinning of test and review costs.
MontiArc is FOCUS [18], a dataflow-based methodology for
the stepwise development and refinement of systems. If the
behavior of a component is described by a MontiArc automata
with input/output, it is implementable (also called realizable) • Extending an ADL and its knowledge base for en-
per construction. For further discussions about foundations abling refinement of lower-level non-deterministic state-
of our methodology, please read also [11]. The semantics of oriented requirement specifications into another state-
(non-deterministic) components are (sets of) stream processing oriented specification by means of transition-refinement
functions [14]. The unique selling point of FOCUS compared and state refinement.
with other concurrents such as π-calculus [19], CSP [20] • Extending counterexample-finding capability for design
or Petri nets [21] is that refinement is fully compositional. error detection.
Thus, one can decompose a system, refine each component • Optimizing signatures of key structures in the knowledge
separately e.g. until an implementation, and then be sure that base to increase the automation degree and reduce the
after composing back the new system will be a refinement needed user-expertise (consisted in rewriting the encoding
of the old one, thus sparing associated testing and integration with total functions instead of partial functions (such as in
costs. It also allows leveraging proof reuse (as will be shown [22]), thus making automatic proof finding much easier)
in the running example section II-G or section II-I). • Integration of an abstraction mechanism called locals,
The contribution of this work is the extension of logic- which improved the efficiency of the code generator
based a knowledge representation for an automatic reasoning about 10 times and enables thus an easier-qualifiable code
approach aiming at reducing certification costs of safety- generator from the ALD to the theorem prover.
critical systems. This is demonstrated through accompanying • Discussing at what extend such a knowledge representa-
the refinement of different abstraction levels of underspecifi- tion approach can scale to meet industrial requirements,
cation (see fig. 1) by verification. The full compositionality of documented in a table in the conclusion after the evalu-
refinement of FOCUS is leveraged for the step-wise refinement ation and consideration of the lessons learned.
of a representative example of a pilot flying system (in this • Providing an Integrated Verification Environment created
cyber-physical system the bus component is hardware and the with Visual Studio Code for the integration of all the
flight guidance component is software). artifacts of the framework (see Appendix).
On a more detailed level, this includes:
• Extending an ADL and its knowledge base for enabling The rest of the papers consists in the following: The next
higher-level history-oriented requirement specification. chapter describes a typical avionics software development
• Extending an ADL and its knowledge base for enabling activity, where step-wise refinements of underspecification
refinement of history-oriented requirement specifications accompanied by verification is presented on the example
into lower-level (closer to implementation, yet still not of a flight guidance system (adapted from a collaboration
necessarily deterministic) state-based requirement speci- between NASA and Rockwell Collins [23], we handle the
fications. more involved asynchronous case).
II. RUNNING E XAMPLE
General Approach
In this section we present the development of a pilot
flying system (PFS) with two flight guidance systems (FGSs)
in a refinable, decomposable fashion, adapted from [23].
While in [23] different levels of abstractions are handled
with different techniques (theorem proving, model checking,
Fig. 2. Verification tool chain comprised of two stages: MontiArc frontend
abstract interpretation), we demonstrate to be able to handle all and Isabelle backend. Specifications are modeled in MontiArc, transformed
abstraction levels by our framework. The red-colored letters to equivalent Isabelle representations, then semantically mapped to Stream
(fig. 1 extracted from certification activities of DO-178C) Processing Functions and their properties are checked highly automatically.
correspond to the sections of the next chapter. During the
formalization of informal requirements, errors in a first version
Below is the first SysReq also as an OCL expression. It is
of the higher-level requirements are detected (red-letters B, C),
formulated in the context of the general component structure
and then repaired (letters I, H). The system to be developed
from fig. 3 and addresses the streams by their port name:
is depicted in fig. 3. The tool chain is described in fig. 2.
The components of the system transmit potentially infinite f s t c1 [ n ] or f s t c3 [ n ]
sequences of messages called streams over its channels [18]. The OCL expression consists of elements known from
Time-synchronous streams are used to model time-sensitive first-order logic. Ports are named after the connected channels
behavior. As described previously in [11], this can be realized from fig. 3. A syntactic extension allows to obtain the nth
through extending the message alphabet by ∼ to denote that element (point in time) of the stream flowing in the channel
no data is transmitted in a time slot. Timing granularity can c1 as c1[n]. The translation as Isabelle theorem looks alike
be set at wish depending on the system to be modeled (e.g. (variables are per default universally quantified). The first
in the case of the flight guidance system below, one time unit item of a tuple is returned by f st.
represents 1 millisecond).
The semantics of components are sets of stream processing
Furthermore, we define a safety-critical sixth SysReq infor-
functions mapping input channel histories to output channel
mally.
histories and are hierarchically decomposable [11].
SysReq6: Pressing and holding the transfer switch c5 for
One-directional channels connect components by transmit-
10 milliseconds always switches the inactive flying side, if
ting input and output messages. In the PFS, messages sent
the inactive component received the last transfer switch input
between the FGSs are transmitted by hardware buses. Each
and the system is in a stable state (see also section C for the
FGS outputs a pair of booleans where the first boolean denotes
architecturial contex).
the liveness of the system and the second boolean is used as
an acknowledgement bit. Clocks restrict the other components B. High-Level Requirements’ (HLR’)
behavior by sometimes forcing them to output the last message
The engineer now tries to develop high-level requirements
and not reacting to its input in any way. The system is
for each sub-component, so that the overall system require-
visualized in fig. 3.
ments can be fulfilled. First, we introduce the high-level
For each component (hardware and software), HLRs and
requirements of the clocks (corresponding in fig. 1 to HLR’):
LLRs were created. When verifying compliance (say between
HLR and SysReqs), the HLRs of all components in the component C l o c k U n f a i r S p e c {
software architecture are proven to fulfill all SysReqs. We timing sync ;
demonstrate to handle in the following a few representa- port
tive certification activities. In our knowledge representation out boolean c l k 1 ;
approach, certification credits concerning ”‘verifiability”’ of
requirements (see fig. 1) are generally claimed by having used spec {
a formal language for the specification, and ”‘accuracy”’ is / / o u t p u t s an i n f . l o n g b o o l s t r e a m
c l k 1 . l e n g t h ( ) = INF
claimed by having formal proofs. }
A. System Requirements (SysReqs) }
The system requirements (SysReqs) are largely adapted The bits on the clocks output stream determine whether
from [23]. By formulating them as Object Constraint Language its associated component is active (executing) or not. The
(OCL) (see [11], [24]) constraints, these can be inputted to the ADL MontiArc is used to define the high-level requirements
tool chain together with the MontiArc system model. It is then (HLRs)of the clock component. This is a component with
checked whether the system model fulfills the requirements. one output and no input channel. First, the timing of the
The first 5 SysReqs are similar to the 5 SysReqs from [23] (see clock is defined. The keyword sync indicates weak-causal
also Appendix). We give the first SysReq in natural language. and causalsync strong-causal time-synchronous components
SysReq1: At least one side is the active pilot flying side. (causality captures realizability in time sensitive modeling,
some technical details concerning the knowledge base see
[25]). The following composition correctly defines the system
Pilot Flying System
model because the composition operator is commutative and
Clock 4
Clock 1 clk4 associative (thus making the composition order irrelevant)
clk1 c4
RL-Bus
c3
[26].
c5 F GSL ⊗ F GSR ⊗ BusLR ⊗ BusRL ⊗ clk1 ⊗ clk2 ⊗ clk3 ⊗ clk4
L-FGS R-FGS
After defining the Pilot Flying System as a composition
c1 c2 clk3
of its sub-components, we define the low-level requirements
LR-Bus
of the sub-components. The unfair clock has to output non-
clk2
Clock 2 Clock 3 deterministicially true or false (input and transition guards can
be modeled in MontiArc [15], but are not present in this
component). A graphical representation of the automata is
given in fig. 4 and the textual version is:
Fig. 3. An architecture of the pilot flying system (PFS), sufficient for
correctly synchronizing the pilot flying sides and the other mentioned system component C l o c k U n f a i r A u t o m a t a {
requirements. clk1 etc. denote the channels that have clocks as sources, c1 timing sync ;
etc. refer to the other communication channels, L-FGS denotes the left flight
guidance system, RL-Bus denotes the bus from right to left. port
out boolean c l k 1 ;
[11]). Weak-causality enforces that the production of an output automaton {
at a point in time t does not depend from an input arriving after / / one s t a t e
the point in time t. Strong-causal components have to define state Single ;
i n i t i a l Single ;
an initial output and delay interaction by 1 time unit. They
are needed for well-defined semantics in feedback loops. The / / o u t p u t s t r u e or f a l s e i n e v e r y s t e p
behavior is specified as a high-level predicate (spec stands S i n g l e −> S i n g l e / { c l k 1 = t r u e } ;
for specification). Inside the spec section, requirements to S i n g l e −> S i n g l e / { c l k 1 = f a l s e } ;
the boolean output stream clk can be formulated as OCL }
}
expressions. The length function obtains the length of a
stream and IN F represents infinity. Timing and interface of the component are defined similar
The HLRs for the Buses and FGSs are defined similarly. to section II-B. The automata then specifies the behavior in
This paper lists only the LLR’ as supplementary material in a lower-level, yet still non-deterministic fashion. States are
fig. 7. defined in the first line of the automata body. The second
line sets the initial state of the automata. Following the state
C. Software Architecture and Lower-Level Requirements’
specifications, the automata transitions and the output and
(LLR’)
state-change behavior are defined on a step-by-step basis.
In fig. 3 each component is represented by a named box.
The channels describe the internal interaction between the D. Compliance of LLR’ to HLR’ and HLR’ Consistency
components. The incoming and outgoind channels are the The consistency of a specification is defined as the existence
global in- and outputs of the PFS. Small boxes represent the of at least one implementation that satisfies the specification.
ports of a component. Our scalable vector graphics (SVG) The consistency of our HLR’ can be shown as follows: First
generator draws figures based on MontiArc models. Such prove the compliance of LLR’ to HLR’ (i.e., LLR’ refines
visualization is a powerful tool to gain overview and improve HLR’). Then show that an implementation of LLR’ exists.
the communication, especially in the early stages of the For the later, consider that LLR’ (e.g. of the clocks) are non-
development process. determinsitic (total) automata, and can easily be converted
Here, each of the 4 clocks is connected to one of the non- to an implementation (deterministic automata) by removing
clock components to model their non-deterministic behavior. transitions responsible for non-determinism. Next, we focus
On a ”‘False”’ clock output signal, each non-clock component on compliance of LLR’ to HLR’.
does not react to its input and simply repeats the last output. For this, the LLR’ MontiArc automata is translated to an
Input channel c5 transmits the transfer switch status, c1 is the Isabelle automata and further transformed to (sets of) stream
output of the L-FGS system and c4 its input from the RL-Bus processing functions. The HLR’ spec is directly transformed
etc. to (a set of) stream processing functions. The transformation
The complete system can be decomposed into sub- from automata to stream processing function (SPF) is defined
components hierarchically [15]. After the translation into as a (greatest) fixed point calculation of the corresponding
Isabelle code, the composition operator ⊗ connects the in- functional [14]. Now, a theorem can be formulated in OCL by
and output channels of two components by its names (for the user, stating: LLR’ refines HLR’. This is translated into
ClockUnfair Automaton reason over not-necessarily-executable specifications [29]. A
counterexample for the 6th SysReq would be e.g. the following
/True
/False
streams on channels c5 and clk3:
streamc5 = F alse1 • T rue11 • F alse∞
streamclk3 = T rue1 • F alse11 • T rue∞
Single The • infix is used for stream concatenation, whereas i-fold
repetition is formalized as i . The stream T rue∞ for example
is an infinitely long stream of messages T rue. Obviously, the
assignment does not contradict the HLR’ of the clock (random
trues and f alses). But the system does not change the flying
Fig. 4. The unfair clock outputs non-deterministically booleans
side after pressing the button for 10 milliseconds (SysReq 6),
as the clock blocks any reaction for 11 time-units. Thus, a
the following Isabelle theorem, where the Isabelle-semantics new and sufficient HLR has to be formulated.
of a MontiArc construct is abbreviated by J...K): The infrastructure for finding counterexamples in our tool
chain has been extended by identifying and inserting (done
theorem as described e.g. in [28]) fitting lemmas into the transformed
”J C l o c k U n f a i r A u t o m a t a K ⊆ J C l o c k U n f a i r S p e c K” Isabelle encoding. These lemmas are essential not only to
So refinement is reduced to a set-inclusion of SPFs. counterexample-finders, but also facilitate automatic proofs
This theorem is proven by showing that every SPF from and general transparency of the encoding.
JClockUnfairAutomataK outputs a bool stream that is infinitely
F. Refinement of HLR’ to HLR
long, thus satisfying the OCL requirement in the spec-behavior
of ClockUnfairSpec. All other components consistencies are As one may notice, one does not have to come up with an
proven similarly and follow the overall tactic to show the entirely new HLR. With only a slight refinement of HLR’,
fulfillment of all specification properties. Since the other the 6th SysReq can be fulfilled. The new clock specification
components are deterministic, their semantics contains exactly (HLR) is obtained by adding the following OCL-predicate into
one SPF. In order to increase automation of reasoning over the spec-body of the ClockUnfairSpec:
(sets of) stream processing functions, abstract (case-study- f o r a l l n i n n a t .
independent) theorems have been proven in the knowledge e x i s t s m in nat .
base [25]. n < m && m < n +10 && c l k [m ] ;
It might be interesting to note that compared to [11], the
largest part of the generator has been moved inside Isabelle. The new HLR restricts the clocks to output at least one
This keeps the inter-language transformation from architecture true every 10 milliseconds. The new specification is called
description language (ADL) to Isabelle minimal (about 10 f air clock and also translated to Isabelle. After generating
times less compared to [11]). This was achieved by integrating the corresponding set of stream processing functions for HLR,
the concept of locales [27]. The whole tool chain becomes thus ”HLR refines HLR’” is reduced to a set-inclusion proof.
easier qualifiable due to the axiomatic and conservative nature theorem
of Isabelle (please note that the translation from a DSL into ”J C l o c k F a i r S p e c K ⊆ J C l o c k U n f a i r S p e c K”
a logical language needs in general to be qualified, and is
usually performed by testing it for a representative collections The signatures of the involved functions are identical, and
of models). the predicate of HLR is a slight sharpening of the predicate
of HLR’ (by the added OCL-requirement in section II-F),
E. HLR’ Compliance with SysReq and thus the refinement proof is easily found automatically.
The next important step is to check the fulfillment of the Since all SPFs from ClockFairSpec output an infinite stream
system requirements. HLR’ fulfills the first 5 SysReqs, but of booleans, the only requirement of the ClockUnfairSpec is
not the 6th. The proofs that HLRs comply with the 5 SysReqs already met.
is generally history-oriented (reasoning over infinite streams).
Meanwhile, tools like quickcheck and nitpick were integrated G. Refinement of LLR’ to LLR
in our tool chain and can be used to automatically search Similar to above, one does not need to come up with an
for counterexamples. Quickcheck originates from Haskell and entirely new LLR (for the clocks) out of their HLR, but
is a test-based tool that needs an executable implementation can instead refine the almost-successful LLR’ just enough to
from which it generates Haskell code and is fast [28]. Nitpick, comply with the HLR. A new LLR for the fair clock is defined
on the other hand, is a SAT-solving based tool that is able as a non-deterministic automata (see fig. 5) using a finite timer
to find even infinitely long stream-counterexamples, and also to force at least one true every 10 milliseconds:
proving the remaining 6th SysReq. This reduces certification
costs of HLR compliance.
Compliance: The compliance with the last SysReq follows
straightforwardly (proof is thus easily found automatically)
from the added OCL-predicate in the spec-body of HLR in
section II-F).
Traceability: Certification credits for the traceability of
HLR is claimed by deleting HLR-predicates (OCL-expressions
from the spec body) one-by-one and proving that each deletion
in isolation already leads to an incompliant system requirement
(one of these cases led to the above mentioned HLR’).
J. Source Code
The non-deterministic clocks can be refined to a determinis-
tic behavior by deleting transitions that offer non-deterministic
Fig. 5. Fair clock with counter choices (e.g. by deleting one of the transitions such as
those occurring in ClockUnfairAutomata). Apart from
the non-deterministic clocks, any LLR of other components
One can save certification costs (of proving compliance
is a deterministic MontiArc model and can be interpreted
of LLR with HLR and SysReq all over again) by proving
as an implementation, since its semantic is a single stream
that LLR is a refinement of LLR’, and then reasoning that
processing function [14].
the already proven properties (LLR’ refines HLR’ and HLR’
fulfills almost all SysReq) will also hold for LLR. This means K. Compliance of Source Code to LLR
one only needs to prove the missing 6th SysReq.
After translating the deterministic components (representing
The refinement of LLR’ into LLR is a refinement between
the source code) to Isabelle, the compliance of source code
non-deterministic automata. Similar to the refinement between
with LLR can be proven. The proof is reduced to showing that
HLR and HLR’, a theorem in Isabelle can be formulated over
the resulting stream processing function (i.e. the semantics of
the automata’s semantics:
the deterministic automata) is an element of the LLR semantics
theorem (a set of SPFs). Accuracy and consistency are correct per
”J C l o c k F a i r A u t o m a t a K ⊆ J C l o c k U n f a i r A u t o m a t a K” construction in the case of a deterministic component. The
compliance of the source code to the software architecture
This is proven by two simple refinement steps. The first one
and to the system requirements holds without further ef-
is a semantics-preserving state-refinement (through splitting
fort by the unique property of FOCUS, that refinement is
the one state of LLR’ into 10 by introducing a counter
fully compositional. Since the other (non-clock) components
variable. The set of behaviors remains after this step the
already were deterministic, their compliance with their LLRs
same (does not become strictly smaller yet) [14] (section
is proven directly.
5.3.5 and 6.4.3). The state refinement is usally a prelude for
subsequent underspecification-reducing refinement steps, such III. C ONCLUSION
as the following. The second and final step is a transition-
In conclusion, the methodology in this paper demonstrated
refinement [14] (section 6.3.1) by which transitions (respon-
handling representative scenarios for a verified development
sible for non-determinism), which lead to ”unfair” behavior
and compositional refinement of safety-critical systems. A
(infinite consecutive inactivity clock-signals) are removed.
developer can specify either directly using a logic language
H. Compliance of LLR to HLR and HLR Consistency (e.g. Isabelle), or using an ADL for distributed systems as
As LLR’ refines HLR’ (section II-D) and LLR refines LLR’ frontend to describe interfaces of the components, their be-
(section II-G), it follows that LLR refines HLR’. Now all that havior and their interaction in a comfortable way. Then the
is left to prove is that LLR satisfies the additional constraints system model and all desired properties can be then translated
of HLR (compared to HLR’). This reduces certification costs into an equivalent specification in a knowledge base created
for the HLR consistency proof significantly. The property that in a logic language.
the state with counter = 0 is reached after maximal 9 steps The developed knowledge base for MontiArc is very general
(visible in fig. 5) is sufficient to prove the additional HLR and can be largely reused for creating knowledge bases for
property easily automatically. other modeling languages (such as AADL, SysML, SCADE,
Simulink etc.) Keeping FOCUS as semantical underpinning
I. HLR compliance with SysReq and Traceability of HLR has the already mentioned advantage that refinement is fully
As HLR’ is already proven to satisfy all but one SysReq and compositional.
HLR is a further refinement of HLR’, we can directly conclude This kind of approach can replace a lot of tests and reviews.
that HLR also satisfies the first 5 SysReq. We thus focus on This helps also with requirements involving always/never,
which cannot be exhaustively verified in general by tests.
Please note though that a certain group of tests and reviews can Soundness Established usually by peer reviews, from 1980-now there
only be complemented hereby, but not completely replaced, for are over 200 papers about FOCUS.
instance checking whether:
The methodology replaces or complements many tests and
• requirements formalization is correct (in general compli- Ability to be integrated into supports fulfilling certification requirements. By relocating
the DO-178x conforming the majority of the code generator internally in Isabelle (we
ance between informal and formal models), process aim over >99%), the tool chain becomes easier qualifiable
due to Isabelle’s axiomatic and conservative nature.
• the methodology is justified and appropriate,
Replaces traditional verification methods throughout the
• requirements and software architecture are compatible Cost savings development life cycle, as seen in the running example (also
see the point below)
with the target computer (unless the target environment Automata Language restricts the user into specifying only
is formally modeled), well-behaved implementable functions (vs expect user to
write realizability proofs)
• a requirement has not been forgotten,
Correctness by construction Underlying methodology FOCUS: Refinement fully
• there is no unidentified dead or deactivated code. compositional – After decomposing a system, refining the
components separately, and composing back, the new
As can be seen in fig. 1, a lot of development and certifi- system is a refinement of the old one (no new (unwanted)
cation costs can be saved by omitting coming up with Source behaviors are added, thus sparing test and integration costs)
Code’ out of LLR’, since it would not be correct anyway, Verification: Compatibility of composition with refinement
Scalability: Compositional allows modularizing and breaking down the proof complexity
because HLR’ are not good enough. One could have even verification of representative industrial-sized models (as in the running
spared the effort of creating LLR’ by the following reasoning: example)
HLR’ has to fulfill SysReqs and to be consistent. In our case
Expressivity of specification Automata language can represent all implementable Stream
we went first for consistency. Instead, by leveraging the higher- language Processing Functions (semantical mapping is surjective,
proof in [9])
level history-oriented spec-infrastructure of our methodology, Timing aspects and
before one takes care of consistency, one could have shown underspecification Supported as presented in the running example
refinement
first that high-level spec’s and the architecture violate SysReqs A user-friendly frontend language and a high-level API in the
(and these kind of proofs are generally history-oriented, thus Usability by normal software knowledge base helps (for hiding low-level engine concepts)
engineers on normal
much easier than induction-based proofs of inductively, state- machines A large amount of encoded lemmas helps aiming for high
automation (which implies less user expertise needed) - see
oriented LLR automata proofs [14]). Then one does not need demo in: https://www.youtube.com/watch?v=krl4Q7MAAlo
to prove HLR consistency (which involves coming up with
LLR automata and showing their compliance to HLR), since
they will be not good enough.
Concerning lessons learned, an interesting observation is
Fig. 6. Industrial requirements
that there are a couple of reasons for preferring the specifica-
tion of components by means of an ADL ideally in a state-
based fashion (coupled with a generator), rather then giving be needed to make it a standard in the tool box of software
the user just an encoding of the stream data type and set of engineering development processes.
theorems over streams in Isabelle:
• The ADL is for a user more comfortable than writing
R EFERENCES
recursive (specified typically as least fixed points [30])
stream processing functions in Isabelle. [1] A. Brahmi, D. Delmas, M. H. Essoussi, F. Randimbivololona, A. Atki,
• The input/output automata of this work are designed and T. Marie, “Formalise to automate: deployment of a safe and cost-
efficient process for avionics software,” in 9th European Congress on
to describe realizable components per construction (and Embedded Real Time Software and Systems (ERTS 2018), (Toulouse,
only these). France), Jan. 2018.
• The automata of our methodology are general enough [2] D. Delmas, E. Goubault, S. Putot, J. Souyris, K. Tekkal, and F. Védrine,
“Towards an industrial use of fluctuat on safety-critical avionics soft-
to represent every realizable stream processing function ware,” in International Workshop on Formal Methods for Industrial
(proof in [14]). Critical Systems, pp. 53–69, Springer, 2009.
[3] E. Payet and F. Spoto, Checking Array Bounds by Abstract Interpretation
Finally, the table in fig. 6 summarizes how the methodology and Symbolic Expressions, pp. 706–722. 06 2018.
presented in this paper handles the industrial requirements [4] T. Bochot, P. Virelizier, H. Waeselynck, and V. Wiels, “Model checking
described in the introduction. The biggest challenge encoun- flight control systems: the airbus experience,” pp. 18 – 27, 06 2009.
[5] S. P. Miller, A. C. Tribble, M. W. Whalen, and M. P. E. Heimdahl,
tered is having a proof being found automatically in a large “Proving the shalls: Early validation of requirements through formal
model. The mitigation of this is an ongoing work consisting methods,” Int. J. Softw. Tools Technol. Transf., vol. 8, no. 4, pp. 303–
in increasing the number of general theorems over dataflow- 319, 2006.
based systems (which are identified intellectually during ver- [6] X. Diao, B. Liu, and S. Wang, “A survey of avionics analysis and
simulation based on aadl model,” Int. J. Inf. Commun. Techol., vol. 9,
ifying case studies), and also exploiting the rapid increase of pp. 282–299, Jan. 2016.
computational capability by using a central web-based high- [7] F. Mhenni, J.-Y. Choley, N. Nguyen, and C. Frazza, “Flight control
performance service to perform the proof search. system modeling with sysml to support validation, qualification and
certification,” IFAC-PapersOnLine, vol. 49, pp. 453–458, 12 2016.
However the application of reasoning over knowledge bases [8] B. Albert, H. Usach, J. Vila, and A. Crespo, “Development of integrated
is still not mature enough and further research and time will modular avionics applications based on simulink and xtratum,” 05 2013.
A PPENDIX
[9] G. Berry, A. Bouali, X. Fornari, E. Ledinot, E. Nassor, and R. de Simone,
“Esterel: a formal method applied to avionic software development,”
Science of Computer Programming, vol. 36, no. 1, pp. 5 – 25, 2000.
[10] P. Caspi, D. Pilaud, N. Halbwachs, and J. Plaice, “Lustre: A declarative FGS LLR
BUS LLR
language for programming synchronous systems,” in POPL, 1987.
[11] S. Kriebel, D. Raco, and B. Rumpe, “Model-Based Engineering for
Avionics: Will Specification and Formal Verification e.g. Based on
Broy’s Streams Become Feasible?,” in [Software Engineering (SE)
und Software Management (SWM), SE SWM, 2019-02-18 - 2019-02-
22, Stuttgart, Germany], pp. 87–94, BMW Group, Chair of Software
Engineering at RWTH Aachen, Feb 2019.
[12] J. Souyris, “Formal methods at airbus: Experience feedback,” 2012.
[13] K. Hölldobler and B. Rumpe, MontiCore 5 Language Workbench Edition
2017. Aachener Informatik-Berichte, Software Engineering, Band 32,
Shaker Verlag, December 2017.
[14] B. Rumpe, Formale Methodik des Entwurfs verteilter objektorientierter
Systeme. PhD thesis, Zugl.: München, Techn. Univ, Zugl. München,
1996.
[15] A. Haber, J. O. Ringert, and B. Rumpe, MontiArc - Architectural mod-
eling of interactive distributed and cyber-physical systems, vol. 2012,3
of Technical report / Department of Computer Science, RWTH Aachen.
Aachen and Hannover and Göttingen: RWTH and Technische Infor- Fig. 7. Supplementary model: Automata for a Flight Guidance System
mationsbibliothek u. Universitätsbibliothek and Niedersächische Staats- component and a Bus. Both MontiArc explicit states (circles) and implicit
und Universitätsbibliothek, 2012. states (variables inside the circles) are indifferently translated in Isabelle as
[16] T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL: A proof elements of the state space. In the Bus lastOut is a variable to save the last
assistant for Higher-Order Logic, vol. 2283 of Lecture notes in artificial output message and in is the input message.
intelligence. Berlin [etc.]: Springer, 2002.
[17] D. Harel and B. Rumpe, “Meaningful modeling: What’s the semantics
of ”semantics”?,” Computer, vol. 37, pp. 64 – 72, 11 2004. SysReq 2..5
[18] M. Broy and K. Stølen, Specification and development of interactive
systems: Focus on streams, interfaces, and Refinement. New York: • The System is in a stable situation whenever both FGSs
Springer, 2001. acknowledgements are true. If the system is in a stable
[19] R. Milner, Communicating and mobile systems: the pi calculus. Cam-
bridge university press, 1999.
state, then at most one side is the active pilot flying side.
[20] C. A. R. Hoare, “Communicating sequential processes,” in The origin • Pressing the transfer switch changes the inactive side,
of concurrent programming, pp. 413–443, Springer, 1978. if the system is in a stable state and the inactive side
[21] W. Reisig, Petri nets: an introduction, vol. 4. Springer Science &
Business Media, 2012.
receives the input.
[22] J. O. Ringert and B. Rumpe, “A Little Synopsis on Streams, Stream Pro- • In the beginning one side has to be the active pilot flying
cessing Functions, and State-Based Stream Processing,” Int. J. Software side. Without loss of generality we choose the left side
and Informatics, vol. 5, no. 1-2, pp. 29–53, 2011.
[23] D. Cofer and S. Miller, “Do-333 certification case studies,” in NASA
to be active. The right side has to be inactive.
Formal Methods (J. M. Badger and K. Y. Rozier, eds.), (Cham), pp. 1– • Only switch to inactive side, if transfer switch is pressed.
15, Springer International Publishing, 2014.
[24] J. Warmer, A. Kleppe, T. Clark, A. Ivner, J. Högström, M. Gogolla,
M. Richters, H. Hussmann, S. Zschaler, S. Johnston, D. Frankel, and
C. Bock, Object Constraint Language 2.0. 01 2001.
[25] J. C. Bürger, H. Kausch, D. Raco, J. O. Ringert, B. Rumpe, S. Stüber,
and M. Wiartalla, “Towards an Isabelle Theory for distributed, interactive
systems - the untimed case,” Tech. Rep. AIB-2020-02, RWTH Aachen,
Jan. 2020.
[26] M. Broy and B. Rumpe, “Modulare hierarchische Modellierung als
Grundlage der Software- und Systementwicklung,” Informatik-Spektrum,
vol. 30, no. 1, pp. 3–18, 2007.
[27] C. Ballarin, “Locales and locale expressions in isabelle/isar,” in Interna-
tional Workshop on Types for Proofs and Programs, pp. 34–50, Springer,
2003.
[28] L. Bulwahn, “The new quickcheck for isabelle: random, exhaustive and
symbolic testing under one roof,” pp. 92–108, 12 2012.
[29] J. C. Blanchette and T. Nipkow, “Nitpick: A Counterexample Generator
for Higher-Order Logic Based on a Relational Model Finder,” in
Interactive Theorem Proving (M. Kaufmann and L. C. Paulson, eds.),
(Berlin, Heidelberg), pp. 131–146, Springer Berlin Heidelberg, 2010.
[30] B. C. Huffman, HOLCF ’11: A definitional domain theory for verifying Fig. 8. Supplementary: Integrated Verification Environment
functional programs. [Portland, Or.]: Portland State University, 2012.