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.