Early validation of system requirements and design

Universidade do Minho Escola de Engenharia Departamento de Inform´ atica Marcelo Miranda Early Validation of System Requirements and Design December 2019 Universidade do Minho Escola de Engenharia Departamento de Inform´ atica Marcelo Miranda Early Validation of System Requirements and Design Master dissertation Master Degree in Computer Science Dissertation supervised by Jorge Sousa Pinto December 2019 D I R E I TO S D E A U TO R E C O N D I C¸ ˜ O E S D E U T I L I Z A C¸ ˜ A O D O T R A B A L H O P O R T E R C E I R O S Este ´ e um trabalho acad´ emico que pode ser utilizado por terceiros desde que respeitadas as regras e boas pr´ aticas internacionalmente aceites, no que concerne aos direitos de autor e direitos conexos. Assim, o presente trabalho pode ser utilizado nos termos previstos na licenc¸a abaixo indicada. Caso o utilizador necessite de permiss˜ ao para poder fazer um uso do trabalho em condic¸ ˜ oes n˜ ao previstas no licenciamento indicado, dever´ a contactar o autor, atrav´ es do Reposit´ oriUM da Universidade do Minho. Licenc¸a concedida aos utilizadores deste trabalho Atribuic¸˜ ao-CompartilhaIgual CC BY-SA https://creativecommons.org/licenses/by-sa/4.0/ i S TAT E M E N T O F I N T E G R I T Y I hereby declare having conducted this academic work with integrity. I confirm that I have not used plagiarism or any form of undue use of information or falsification of results along the process leading to its elaboration. I further declare that I have fully acknowledged the Code of Ethical Conduct of the University of Minho. ii A C K N O W L E D G E M E N T S I wish to acknowledge the special moments and all the help provided by everyone during this last year and during my academic journey. A special thanks to Professor Jorge Sousa Pinto for the availability and support he granted, but also for our casual conversations. To United Technologies Research Center for the opportunity to join you during this dissertation, and all the people I met there for the great moments and beers we shared together. To Stelios Basagiannis for the support and to Georgios Giantamidis for the extensive guidance and all the great jokes. I want to thank all the professors that guided me during this journey, giving me the tools to better understand this subject that always marvelled me. Finally, I would like to thank my friends for all the truly great moments we shared, as well as the ones that are still to come. For all the support, for putting up with me, and for everything that shall remain unwritten in a dissertation. iii A B S T R A C T Modern society is relying more and more on electronic devices, most of which are embedded systems and are sometimes responsible for performing safety-critical tasks. As the complexity of such systems increases due to concurrency concerns and real-time constraints, their design is more prone to errors which can lead to catastrophic outcomes. In order to reduce the risk of such outcomes, a model-based methodology is commonly used. The model describes the behaviour of the system and is subject to verification techniques such as simulation and model checking in order to verify it behaves according to the requirements. Common problems that arise with this methodology is the ambiguity of requirements written in natural language and the translation of a requirement to a property that can be verified along with the model. This thesis proposes a tool that, after the translation of the requirements to temporal formalism, allows the automatic generation of monitors in order to verify the model. Our target platform is Simulink, which is widely used in this domain to model, simulate and analyze dynamic systems. Keywords: formal methods, runtime monitoring, temporal logics, SALT, SpeAR iv R E S U M O A sociedade de hoje depende cada vez mais de dispositivos eletr´ onicos, a maioria dos quais s˜ ao sistemas embebidos e, por vezes, respons´ aveis pela realizac¸˜ ao de tarefas cr´ ıticas. ` A medida que a complexidade destes sistemas aumenta devido a problemas de concorrˆ encia ou restric¸ ˜ oes de tempo real, o design torna-se mais suscet´ ıvel a erros que podem levar a resultados catastr´ oficos. A fim de reduzir estes riscos, recorre-se a uma metodologia de desenvolvimento baseada em modelos. O modelo descreve o comportamento do sistema e pode ser sujeito a t´ ecnicas de verificac¸˜ ao, tais como simulac¸˜ ao ou model checking, a fim de verificar que este exibe o comportamento descrito nos requisitos. Problemas comuns que surgem com esta metodologia devem-se ` a ambiguidade dos requisitos, tipicamente escritos em linguagem natural, e ` a traduc¸˜ ao destes para uma propriedade que pode ser verificada em conjunto com o modelo. Esta dissertac¸˜ ao prop˜ oe uma ferramenta que, ap´ os a traduc¸˜ ao dos requisitos para uma linguagem de especificac¸˜ ao formal, permite a gerac¸˜ ao autom´ atica de monitores para verificar o modelo. A plataforma para a qual os monitores s˜ ao gerados ´ e o Simulink, que ´ e tipicamente utilizado neste dom´ ınio para modelar, simular e analisar sistemas dinˆ amicos. Palavras-chave: m´ etodos formais, l´ ogicas temporais, runtime monitoring, SALT, SpeAR v C O N T E N T S 1 introduction 1 1.0.1Motivation 2 1.0.2Objectives 2 2 background 4 2.1System requirements 4 2.1.1Specifying requirements 5 2.2Model based engineering 5 2.2.1Runtime monitoring 6 2.2.2Transition System 7 2.3Temporal Logics 9 2.3.1Linear Temporal Logic 11 2.3.2Past LTL 12 2.3.3Property Patterns 14 2.3.4SpeAR 16 2.3.5SALT 18 2.4Simulink 19 3 the monge tool 21 3.1Tool overview - Requirement formalisation 22 3.2Tool overview - Requirement extraction 23 3.3Tool overview - Monitor example 24 3.4Design decisions 25 4 monge architecture 27 4.1Runtime verification with monitors 28 4.1.1Deterministic Finite Automaton 31 4.1.2Monitoring with Past Formulas 33 4.2From a specification language to a monitor 37 4.2.1SpeAR 38 4.2.2SALT 40 4.3Extraction DSL 42 4.4Final results 43 5 conclusion 46 5.1Future work 46 vi L I S T O F F I G U R E S Figure 1Comparison between testing and runtime monitoring. 7 Figure 2Transition System 8 Figure 3Patterns scopes. Figure reproduced from Dwyer et al. (1999). 15 Figure 4Patterns hierarchy that includes real-time patterns. Figure based on Konrad and Cheng (2005). 16 Figure 5Outport and Inport blocks 19 Figure 6Goto and From blocks 20 Figure 7Delay block 20 Figure 8MATLAB Function block 20 Figure 9Chart block 20 Figure 10 Example of a generated monitor with its different components highlighted. 25 Figure 11 Tool architecture 27 Figure 12 Example of a deterministic finite automaton. 32 Figure 13 Past LTL semantics for formula H p.33 Figure 14 Recursive Past LTL semantics for formula H p.34 Figure 15 Rough example of the process that formal specifications go through. 37 vii 2.2. Model based engineering 7 When a simulation is running, it is possible to extract information from it and check if certain properties are violated or hold, a technique known as runtime monitoring.Offline monitoring expects monitors to check formulas against simulation traces, while in online monitoring the monitor is running in parallel with the simulation. We classify the monitor as active if it also affects the simulation inputs and classify it as passive otherwise. Online monitoring increases the overall time of the running simulation but it can be used to stop a faulty simulation once a property is violated or, in real systems, can be used to prevent dangerous behaviour from happening. The usual approach for runtime monitoring is to synthesise requirement models, i.e. monitors, and couple them to the system model in order to be able to query the execution state. Once the simulation is running the system is verified by the monitors which produce a verdict regarding weather the properties are satisfied or not. To synthesise such monitors, engineers write the properties in a formal specification which can then be automatically translated into the intended monitor. Figure 1: Comparison between testing and runtime monitoring. The most common approach to detect errors during simulations is unit testing. By providing pairs of input/output it is possible to check if for a given input the simulation produces the expected output. For complex systems, however, it is not trivial to discover the correspondent output to a given input and thus this task would not be easily automated. Hence why we rely on runtime monitors instead which, by encoding the behaviour the system is expected to exhibit, is able to produce a verdict for all inputs. 2.2.2Transition System There are several approaches to modelling systems, depending on the properties of the system that we want to document or analyse. In the context of formal verification, systems are typically modelled with transition systems. A transition system is a graph that represents the behaviour of a system. Formally, it is defined by TS = (S,Act,→,I,AP,L)where •Sis the set of states, •Act is the set of actions through which the system can evolve, 2.2. Model based engineering 8 •→⊆ S×Act ×Sis the transition relation that evolves the system by transitioning to the next state through an action, •I⊆Sis the set of initial states, •AP is the set of atomic propositions, •L:S→2AP is the labelling function that describes which atomic propositions are satisfied at a given state. The transition system starts in one of the initial states I. Given a state s, if there is an action athat allows the system to evolve to another state s′, such action can be taken through the transition relation sa −→ s′.L(s)is the set of atomic propositions that are satisfied in state S. Apath πis a state sequence that starts in an initial state and is either infinite or ends in a terminal state, i.e. a state with no successors. The set of atomic propositions that are valid along the execution is given by trace(π). π=s0s1s2s3..sn trace(π) = L(s0)L(s1)L(s3)..L(sn) Temporal logics typically consider only infinite transition systems, i.e. transition systems without terminal states. A finite TS can be transformed into an infinite TS by introducing a new transition from the terminal state to a trap state. Trap states have a self-loop and do not satisfy any atomic propositions. a s1 {p, q} c a s2 {t} s3 {p, q} s4 b Figure 2: Transition System In Figure 2the TS starts in the initial state s1, where {p,q} ⊆ AP evaluates to true. From s1, the system can only evolve to s2through s1 a −→ s2. Once the system reaches s2, it can evolve either to the terminal state s3or s4. It is possible for the system to stay forever in the 2.3. Temporal Logics 9 loop s2 c −→ s4 b −→ s2. The action taken is chosen in a non-deterministic way. Some possible paths and the respective traces for this TS are π1=s1s2s4s2s3trace(π1) = {p,q}{t}∅{t}{p,q} π2=s1s2s4s2s4s2. . . trace(π2) = {p,q}{t}∅{t}∅{t}. . . The temporal logics approached in this document abstract away from actions. They are considered state-based, making only use of the atomic propositions of the states to specify system properties. 2.3 temporal logics Temporal logics are extensions of propositional logic that include modal operators to reason about time. In propositional logic, a statement is either true or false and its truth value is constant in time. The truth value of temporal logic statements, however, can vary with time. Temporal logic is widely used in formal verification to describe the evolution of a system over time. For formal analysis to be possible, functional requirements must be expressed as temporal logic formulae. Once the requirements are expressed in temporal logic, the engineer can check if the behaviour exhibited by the model complies with the one described by the specified properties. Properties can be classified in two different categories. Safety-properties state that something bad should never happen and thus are properties that, once they are not satisfied, are considered to have been violated. A property such as ”no two processes can be on a critical section at the same time” is an example of a safety property. Liveness-properties state that something good will eventually happen. Since liveness properties always require that something in the future must hold, such properties cannot be verified on finite traces and therefore are not suitable for runtime monitoring. This contrasts with safety properties in which by observing a finite trace it is always possible to check if they hold or not. An example of a liveness property is ”after the button is pressed, the engine will eventually start”. Different temporal logics consider different properties when reasoning about time. Linear Time Logic (LTL) considers time to be discrete and linear, while Computation Tree Logic (CTL) considers time to be discrete and branching. Metric Temporal Logic (MTL) has a linear and continuous view of time. Let us briefly explain these different notions of time: 1.Discrete: Discrete time is viewed as set of points (or moments) that are equally distant. This is the case of digital clocks that have a fixed clock rating. 2.3. Temporal Logics 10 2.Continuous: In continuous time the distance between two points of time is arbitrary and between any two points, there is an infinite amount of other points. This is typically used when trying to model dynamic systems. 3.Linear: In linear time, for a formula to hold at a given state, it must hold for all possible paths that arise from that state. There is an implicit universal quantification over all the possible computations. 4.Branching: Contrary to a linear view of time, a branching view takes into consideration that a state can have different computations leading to different states and thus different futures. As such, instead of a notion of time based on paths, it considers that for each state there is a tree, rooted in that state, that represents the different computations that can occur. Although several properties can be expressed both in linear and or branching logics, their expressiveness is incomparable and there are properties that can only be expressed in one of them. An instance of a property that can be expressed with a branching view of time but not with a linear one is the property that states that the system should always be able to return to one of its initial states. On the other hand, the property that states eventually, q will hold forever is expressible in a linear view of time but not in a branching one. Temporal logics that consider a discrete view of time such as LTL or CTL are considered qualitative temporal logics and deal mainly with the ordering of events, while logics with a continuous view of time such as MTL are considered quantitative and deal both with the ordering of events and the distance between them (Koymans,1990). Real time systems require the expression of properties such as ϕmust hold within three miliseconds of property ψ, which can only be expressed with quantitative timing. Furthermore, some temporal logics are designed to refer only to the future (Linear Temporal Logic) while others are designed to refer only to the past (Past Linear Temporal Logic). LTL and Past LTL have the same expressive power, i.e they are able to express the same properties. However, some properties can be expressed exponentially more succinctly in a way than the other. This is important not only to ease the job of engineers that are writing properties, but also because the verification time of a property depends on the size of the formula. The temporal logics that will approached in the next sections are LTL and Past LTL. After that, we will also present two specification languages that are intended to leverage the difficulty of writing formal properties by providing a more natural syntax and pattern support, SpeAR and SALT. 2.3. Temporal Logics 11 2.3.1Linear Temporal Logic Through LTL (Pnueli,1977) it is possible to specify linear time properties that specify the traces the system should exhibit. LTL is considered linear due to the fact that, for each moment in time, the future is already predetermined and there is only a single successor state. The following grammar describes the syntactic rules that allow the construction of LTL formulae. ϕ:=true |α| ¬ϕ|ϕ1∨ϕ2| ϕ|ϕ1Uϕ2 where a ∈AP. The formulae are composed of atomic propositions α∈AP; the boolean connectives ¬ and ∨which are enough to obtain the missing boolean connectives such as ∧or →, hence obtaining the full power of propositional logic; the temporal modalities Next (or X) and Until (U). As in propositional logic, we are able to derive the missing operators Finally (♦ or F) and Globally (or G). ♦α:=true U α α:=¬♦¬α Informally, the meaning of the presented temporal modalities can be described in the following manner. •φ— the formula φmust hold in the next state. •φUψ— the formula φmust hold until ψis satisfied. •♦φ— the formula φmust eventually hold in the future. •φ— the formula φmust always hold in the future. LTL properties operate over paths and their respective traces. For a path π, the satisfaction relation (|=path) is defined through the behaviour exhibited by its trace. In turn, for a trace to satisfy (|=trace) a property it must include the behaviour described by the property at hand. π|=ϕiff trace(π)|=ϕ A state satisfies (|=state) a property if, and only if, all the paths starting in that state satisfy the said property. s|=ϕiff ∀π∈Paths(s).π|=ϕ 2.3. Temporal Logics 12 Finally, a system satisfies (|=TS) a given LTL formula if, and only if, all of its initial states satisfy that property. TS |=ϕiff ∀s0∈I.s0|=ϕ The LTL semantics for infinite words over 2AP are defined as follows. σ|=true σ|=αiff α∈A0(i.e. A0|=α) σ|=ϕ1∧ϕ2iff σ|=ϕ1and σ|=ϕ2 σ|=¬ϕiff σ6|=ϕ σ|=ϕiff σ[1 . . . ] = A1A2A3. . . |=ϕ σ|=ϕ1Uϕ2iff ∃j≥0 . σ[j. . . ]|=ϕ2and σ[i. . . ]|=ϕ1, for all 0 ≤i<j And for the derived operators ♦and . σ|=♦ϕiff ∃j≥0 . σ[j. . . ]|=ϕ σ|=ϕiff ∀j≥0 . σ[j. . . ]|=ϕ Let us consider a system with two concurrent processes that share a critical section and require mutual exclusion. The safety property No two processes can be in the critical section at the same time is easily expressible with LTL by resorting to the set of atomic propositions critnthat stand for Process n is in the critical section ¬(crit1∧crit2) and the liveness property that guarantees that at least one of the processes is capable of continuously reaching the critical section. ♦crit1∨♦crit2 Unless we guarantee that the system behaves fairly, it is not possible to specify that both processes can reach the critical section infinitely often. 2.3.2Past LTL According to Barringer et al. (1996) past-time modalities do not add expressiveness power to pure future temporal logics which led to languages dropping such modalities in linear time temporal logic for the sake of simplicity. More recent research (Markey,2003) shows, however, that although no expressive power is lost, there are classes of properties that can 2.3. Temporal Logics 13 be expressed exponentially more succinctly with past operators. Succinct formulas, besides being more intuitive for engineers, produce smaller automatas. The following grammar describes the syntactic rules that allow the construction of Past LTL formulae. ϕ:=true |α| ¬ϕ|ϕ1∨ϕ2|Yϕ|ϕ1Sϕ2 where a ∈AP. The grammar is similar to that of LTL with temporal modalities Next and Until are replaced by the temporal modalities Previous (Y) and Since (S). As in LTL, we are able to derive the missing operators Previously (P) and Historically (H). Informally, the presented temporal modalities can be described in the following manner. •Yφ— the formula φmust have been satisfied in the previous state. •φSψ— the formula φmust hold since the moment ψwas satisfied. •Pφ— the formula φmust have been satisfied sometime in the past. •Hφ— the formula φmust have been satisfied in all the previous states. The formal semantics of the Past LTL operators for finite traces are defined as follows. σ|=true σ|=αiff α∈A0(i.e. A0|=α) σ|=ϕ1∧ϕ2iff σ|=ϕ1and σ|=ϕ2 σ|=¬ϕiff σ6|=ϕ σ|=Yϕiff σ′|=ϕ, where σ′=σn−1if n>1 and σ′=σif n=1 σ|=ϕ1Sϕ2iff σj|=ϕ2for some 1 ≤j≤nand σi|=ϕ1for all j<i≤n σ|=Pϕiff ∃j. 1 ≤j≤n.σj|=ϕ σ|=Hϕiff ∀j. 1 ≤j≤n.σj|=ϕ An important observation that has an impact on monitoring algorithms is that the above semantics can also be defined recursively. If the satisfaction relation for a formula and a trace is calculated along its execution, this allows us to calculate the satisfaction relation for the next step by only looking to the previous step. σ|=ϕ1Sϕ2iff σ|=ϕ2or (n>1 and σ|=ϕ1and σn−1|=ϕ1Sϕ2) σ|=Pϕiff σ|=ϕor (n>1 and σn−1|=Pϕ) σ|=Hϕiff σ|=ϕand (n>1 implies σn−1|=Hϕ) 2.3. Temporal Logics 14 2.3.3Property Patterns Formal verification techniques are still not widely adopted. A common obstacle that is slowing down adoption is the required expertise necessary to write properties. Furthermore, the resulting formulae are often hard to read and even harder to write. To make matters worse, a person entering the field for the first time is usually faced with a lack of both good training materials and good tool support. The introduction of a pattern system created by expert system designers aims to reduce the background experience required for new users. Design languages, as well as programming languages, are usually very expressive, allowing for a wide-variety of solutions to a problem,with their respective pros and cons that need to be evaluated. Most of the times, however, users prefer guidance over expressiveness. With that in mind and based on the design patterns solution which is widely used in the programming world, pattern systems for specifications that match common requirements into specification templates were created. These systems comprise a collection of high-level abstractions over specifications that can be mapped to many different formalisms such as LTL or CTL. A pattern captures a solution that appears repeatedly when solving design problems. It seeks to gather information around both the problem and the solution, documenting the context in which it appears, the requirements it addresses, how it solves the problem, and when the pattern should be used. The patterns are formalism-agnostic and can be parameterised by individual states or even nested formulae in order to obtain a concrete specification. It is important to note that even though a pattern can be expressed in multiple formalisms, the resulting formulae are not necessarily equivalent due to the differences in the semantic models of each formalism. Pattern system by Dwyer The pattern system described in Dwyer et al. (1999) is a collection of simple patterns defined with the intention of easing the use of formal methods in practice. The patterns are divided according to their nature into two categories dealing with either the occurrence of states or the ordering of states. In the first category, dealing with occurrence, we have: •Absence — The state formula does not occur within the scope. •Existence — The state formula must occur within the scope. •Bounded existence — The state formula must occur ktimes within the scope. Variants of this pattern specify at most k occurrences and at least k occurrences. •Universality — The state formula occurs throughout the scope. In the second category, dealing with ordering, we have: 2.3. Temporal Logics 15 •Precedence — A state Pmust always be preceded by a state Qwithin the scope. •Response — A state Pmust always be followed by a state Qwithin the scope. •Chain precedence — A sequence of states P1, .., Pnmust always be preceded by a sequence of states Q1, .., Qn. This pattern is a generalisation of the precedence pattern. •Chain response — A sequence of states P1, .., Pnmust always be followed by a sequence of states Q1, .., Qn. This pattern is a generalisation of the response pattern. Each pattern has a scope which can be the entire program or just a fragment and is defined by a starting state and/or an ending state. The scopes described in Dwyer et al. (1999) are the following: global (over the entire program), before (the execution up to a given state), after (the execution starting at a given state), between (the execution between two states), and after-until (similar to the between scope but the ending state is not guaranteed to occur). Figure 3: Patterns scopes. Figure reproduced from Dwyer et al. (1999). A pattern is composed by several fields such as its intent and the problem it addresses, mappings to multiple formalisms such as LTL and CTL, as well as examples and concrete situations in which they were used. Additionally, some patterns describe their relation to other patterns, for instance, the absence pattern is the dual of the existence pattern and the chain response is a generalisation of the response pattern. Dwyer provides some notes on property specification using the pattern system he developed. In these notes he explains how to adapt the existing patterns to better express the desired property by addressing topics such as the combination of patterns, variations in the scopes and pattern parameterisation. Out of the 555 examples of property specifications Dwyer collected to evaluate his pattern system, 92% were considered to be an instance of one of the provided patterns. The patterns developed by Dwyer et al. (1999) inspired many other works such as a modified version of the pattern system that extends it to support real-time properties by 2.3. Temporal Logics 16 Konrad and Cheng (2005) or instantiations of the patterns into timed observer automata by Gruhn and Laue (2006). Specification Quantitative Duration Periodic Real-Time Order Minimum Duration Maximum Duration Bounded Recurrence Bounded Response Bounded Invariance Qualitative Order Response Precedence Chain Response Chain Precedence Occurrence Universality Existence Absence Bounded Existence Pattern Category Type Figure 4: Patterns hierarchy that includes real-time patterns. Figure based on Konrad and Cheng (2005). This work also contributed to the emergence of high-level specification languages that include both patterns and scopes in its features. Next, we present two examples of such languages, SpeAR and SALT, which provide a grammar close to a structured natural language to improve readability and intuitiveness when reading and writing properties. 2.3.4SpeAR SpeAR (Specification and Analysis of Requirements) is an open-source tool for capturing and analysing requirements stated in a language that is formal, yet designed to read like natural language (A. Fifarek,2017). The SpeAR specification language has the formal semantics of Past LTL and supports basic arithmetic, logical, and relational operators. The SpeAR developers sought to provide a specification language as natural as possible so that engineers could express themselves more naturally. Hence, SpeAR provides english aliases for most logical operators. The following is an example of a requirement written using the SpeAR specification language. if signal greater than threshold then output equal to ON Spear documents have a well-defined structure that promotes the grouping of requirements to enable modularity and reuse. A SpeAR document distinguishes inputs,outputs, state,assumptions,requirements and properties. •Inputs, Output, State: These parts of the document describe the data that is handled throughout the system. Inputs represent monitored or observed data from the environment as well as inputs from other components. Outputs represent data sent to 3.2. Tool overview - Requirement extraction 23 In the example portrayed in 3.1there are six different requirements. Each requirement has an id, a description and its respective specification. REQ 1and REQ 5were specified as SpeAR formulas. REQ 6was specified as a SpeAR pattern. REQ 2and REQ 4were specified as SALT formulas. REQ 3is a performance requirement and thus was ignored. 3.2 tool overview -requirement extraction Requirements are usually written in a natural language and archived in digital formats that focus on readability instead of structure. Hence, requirement documents are rarely suited for analysis and computations and thus there is a necessity to extract requirements into a more treatable form from such documents. Regular expressions are the common solution to extract segments from a text document. By defining a search pattern that describes the data we seek, regular expressions allow us to find all the substrings of the document that match such pattern. However, we do not consider this technique a good solution for requirement engineers. Regular expressions require some expertise to write, are hard to compose and, due to their succinct syntax, are difficult to read. Thus, we developed a simple DSL that addresses the described issues. keywordstyle keywordstyle keywordstylekeywordstyle identifier = "REQ_" keywordstylekeywordstyle followed_by one_or_more digit keywordstylekeywordstyle keywordstylekeywordstyletext = one_or_more any_char keywordstylekeywordstyle keywordstylekeywordstylerequirement = capture identifier keywordstylekeywordstyle followed_by ":" keywordstylekeywordstyle followed_by zero_or_more whitespace keywordstylekeywordstyle capture text keywordstylekeywordstyle followed_by new_line keywordstyle keywordstyle Listing 3.2: Example of an extractor using the developed DSL. The extractor in Example 3.2is compiled to (REQ [0−9]+) :\s∗(.+)\n{2}, which is the regular expression we would use underneath to extract the requirements listed in 3.3. Each expression denotes an extractor. The tool expects a final extractor that captures an identifier for the requirement as well as the requirement text. In this example, the requirement extractor starts by capturing the identifier, relying on identifier extractor that was previously defined, which expects the keyword REQ followed by one or more digits. In order to match a requirement, the identifier should be followed 3.3. Tool overview - Monitor example 24 by a colon and optional whitespace. All characters are then considered to be part of the requirement text, as defined in the text extractor until a new line is met. keywordstyle keywordstyle keywordstylekeywordstyle REQ_1: When the system is in state_1 and signal_3 + signal_2 > 100, the system shall keywordstylekeywordstyletransition to state state_3. keywordstylekeywordstyle keywordstylekeywordstyleREQ_2: Once the system is in state_3 occurs, then the system will be in state_4 keywordstylekeywordstylesomewhere in the future. keywordstyle keywordstyle Listing 3.3: Excerpt of a fake requirements document that is extractable with the extractors defined in the Listing 3.2. 3.3 tool overview -monitor example It is important to note that while SpeAR translates to Past LTL, SALT can translate to either Past LTL or LTL depending on what features were used in the specification. While Past LTL based monitors and LTL based monitors are similar in structure, the underlying verification algorithm is different. Past LTL also requires an extra layer to deal with the previous operator Y, which looks to the value of an expression in the previous state. More details on the verification algorithms are given in Section 4.1. Figure 10 shows the structure of the generated monitors. In the following paragraphs the purpose of each component is explained. •Signal extraction (orange) - The needed signals are extracted from the model and linked into Goto blocks so that they can be accessed through From blocks in the rest of the monitor. This intends to reduce the number of transitions as well as the reducing the coupling of the monitor to the model by extracting all the required data from the model only once and in a single place. •Previous layer (purple) - In the case of Past LTL it is possible for expressions to refer to previous values of a signal. Therefore we need an extra layer that links the original signal into a Delay block to obtain the values from previous states. As in the Signal extraction layer, these blocks are linked into From and Goto blocks to reduce transitions throughout the monitor. •Mathematical expressions (green) - Math expressions need to be computed into boolean values before passing them to the runtime monitoring algorithm. For each math expression we add a MATLAB Function block that gets their parameters through From blocks and outputs a boolean value with the result of the expression. The constants used inside the expressions are defined in the MATLAB script generated by the tool. 3.4. Design decisions 25 Figure 10: Example of a generated monitor with its different components highlighted. •Stateflow (red) - The Stateflow block encapsulates the runtime verification algorithm and it is where the main difference between LTL and Past LTL monitors lies. The algorithms are described later in Section 4.1. The Stateflow outputs the monitor verdict for that point in time. •Output (blue) - The output layer simply exposes the monitor verdict to other systems in the model. 3.4 design decisions While developing the tool we made some design choices that affect the way requirements can be written. We will now elaborate on these. 1. SpeAR and SALT do not offer the same features. We do not intend to introduce the lacking features since the purpose of supporting multiple languages is for them to 3.4. Design decisions 26 cover for each other. However, mathematical expressions are an example of something we want to have support for in all the languages we support. 2. Since the purpose of the tool is to generate runtime monitors, it is important to interoperate with the Simulink model. Thus, when writing the specification the engineer should take care to name the variables present in the specifications with the same names as the equivalent Simulink signals. 3. For simplicity, every specification is handled individually and there is no notion of a SpeAR document or SALT document. This makes it impossible for the engineer to use some of the features SpeAR and SALT provide, such as user-defined patterns. Section 4.2provides more details on why this decision was necessary. Temporal logics usually support only boolean values and boolean operators. However, it is common for functional requirements to rely on arithmetic operations to express behaviour. While SpeAR supports such operators, SALT does not. SALT provides, however, quoted boolean propositions whose interpretation can be customised. We make use of such propositions to handle mathematical expressions. keywordstyle keywordstyle keywordstylekeywordstyle assert always (if ’state == STATE_3’ then eventually ’state == STATE_4’) keywordstyle keywordstyle Listing 3.4: SALT specification with quoted boolean expressions and named constants. keywordstyle keywordstyle keywordstylekeywordstyle historically if previously state equal to STATE_1 and signal_3 + signal_2 > 100 then keywordstylekeywordstylestate equal to STATE_3 keywordstyle keywordstyle Listing 3.5: SpeAR specification with built-in math operators. It is also common for engineers to use named constants in their requirements to express the set of values a signal can be evaluated to. In order to differentiate constant names from signal names, signal names are expected to be lower case identifiers while named constants are expected to be upper case identifiers. 4 M O N G E A R C H I T E C T U R E The MonGe architecture is divided in two different packages: an extraction package and a backend package. Figure 11: Tool architecture The extraction package is a simple one. It defines the grammar and the translation from the DSL to regex patterns. The backend, on the other hand, needs to provide two different abstractions for the verification algorithm: one based on deterministic finite automatons (DFA) and another based on the recursive semantics of past LTL. These algorithms are built on top of a monitor abstraction that contains all the data obtained by parsing the formula. Based on this data, the monitor abstraction is able to render the MATLAB script that builds the runtime monitor for the formula. The rendering of the Stateflow block is left outside the scope of this abstraction, allowing for other abstractions to be built on top of this one, implementing different verification algorithms. This is the case of the PastFormula abstraction, that implements the rendering of the Stateflow block for the recursive semantics of Past LTL and the DFA abstraction that does the same for the algorithm based on deterministic finite machines. 27 4.1. Runtime verification with monitors 28 Furthermore, the backend module contains two inner packages, one for each of the specification languages supported. SpeAR always relies on past semantics, however it is possible to write SpeAR specifications by either using their grammar or by using the builtin patterns they provide. The spear package provides the necessary modules to parse the grammar (SpearLexer and SpearParser) and extract the necessary data required by PastFormula (SpearFormula and SpearDocument). For SpeAR patterns, which have a well know translation into DFAs and thus rely on the DFA based verification algorithm, there is an abstraction (SpearPattern) that handles the same data extraction. The patterns package contains the translation from every pattern into a DFA. A SALT formula can rely either on future or past semantics. The formula is fed to the SALT compiler and then, depending on the semantics used, the next steps may differ. In the case of future semantics, the SALT compiler outputs LTL that is then handled by Spot – a tool that is able to output a DFA in the Hanoi Omega Automata (HOA) format from an LTL expression. Such output is then parsed and converted into a state machine for Simulink. In the case of past semantics, the SALT compiler outputs the formula in an intermediate format which is then subject to a process similar to the one that SpeAR formulas go through. Finally, the backend provides a requirement module that integrates the entire backend, being able to generate a monitor from a text specification that can be either SALT or SpeAR. 4.1 runtime verification with monitors In this section we will dive again into the monitoring and understand how data flows from the system model into the Stateflow block that encapsulates the verification algorithm. These algorithms are responsible for checking, based on the data obtained from the previous layers, if the property holds or not. Thus, this is the part of the monitor that actually encodes the behaviour we expect the system to exhibit, as described in the temporal formula. As mentioned before, data is extracted from the system model using From blocks with the signal names that appear in the formula. In Past LTL it is possible to refer to values of signals from previous states. In such cases, the signals go through a Delay block that delays the value as many steps as necessary. With this, we have all the values we need to evaluate the mathematical expressions that appear in the formula. By evaluating the mathematical expressions we eliminate all arithmetic expressions, ending up with just boolean values which are the only data type that our verification algorithms can reason about. The monitor abstraction provides a way to describe a runtime monitor and generate a MATLAB script that builds the Simulink model for that monitor. As expected, most of the parameters match the various layers that exist in the model: 4.1. Runtime verification with monitors 29 1. the set of signals that need to be extracted from the system model; 2. the set of signals that need to be delayed due to the semantics of the Past LTL PRE operator; 3. the mathematical expressions that need to be evaluated and their respective inputs; 4. the constants that appear in the temporal formula and need to be defined as a MATLAB value. This abstraction however is just a building block that must be extended for each verification algorithm we use by providing the logic to render the respective Stateflow chart that is encapsulated in the Stateflow block. The following is a template of the generated script that is instantiated with the data extracted from the specifications. Note that there are several parts that just deal with the positioning of elements in the chart. keywordstyle keywordstyle keywordstylekeywordstyle sfnew; keywordstylekeywordstylert = sfroot; keywordstylekeywordstylemodel = rt.find(’-isa’,’Simulink.BlockDiagram’); keywordstylekeywordstylech = model.find(’-isa’,’Stateflow.Chart’); keywordstylekeywordstyleset_param(’untitled/Chart’,’position’, [1000, 500, 1150, 650]); keywordstylekeywordstyle keywordstylekeywordstyle{% for arg in args %} keywordstylekeywordstyleadd_block(’simulink/Sources/In1’,’untitled/{{ arg }}’); keywordstylekeywordstyleadd_block(’simulink/Signal Routing/Goto’,’untitled/GOTO_{{ arg }}’) keywordstylekeywordstyleadd_line(’untitled’,’{{ arg }}/1’,’GOTO_{{ arg }}/1’); keywordstylekeywordstyle keywordstylekeywordstyleset_param(’untitled/{{ arg }}’,’position’, [{{ 300 * loop.index }}, 50, {{ 300 * keywordstylekeywordstyle loop.index + 20 }}, 70]); keywordstylekeywordstyleset_param(’untitled/GOTO_{{ arg }}’,’position’, [{{ 300 * loop.index + 100 }}, 40, keywordstylekeywordstyle{{ 300 * loop.index + 140 }}, 80]); keywordstylekeywordstyleset_param(’untitled/GOTO_{{ arg }}’,’GotoTag’,’{{ arg }}’) keywordstylekeywordstyle{% endfor %} keywordstyle keywordstyle It starts by creating a new Simulink model with an empty Stateflow block and defines some variables. Next, it goes through all the signals (args) that are needed from the system model and creates a pair of Input block and Goto block for each one, setting the necessary parameters and connecting them. With this we are able to access all signals throughout the rest of the model while avoiding cluttering the model with connections. keywordstyle keywordstyle keywordstylekeywordstyle {% for p in previous %} keywordstylekeywordstyleadd_block(’simulink/Signal Routing/From’,’untitled/FROM_{{ loop.index }}’) keywordstylekeywordstyleadd_block(’simulink/Commonly Used Blocks/Delay’,’untitled/DELAY_{{ p.0 }}’) 4.1. Runtime verification with monitors 30 keywordstylekeywordstyleadd_block(’simulink/Signal Routing/Goto’,’untitled/GOTO_PRE_{{ p.0 }}’) keywordstylekeywordstyle keywordstylekeywordstyleadd_line(’untitled’,’FROM_{{ loop.index }}/1’,’DELAY_{{ p.0 }}/1’); keywordstylekeywordstyleadd_line(’untitled’,’DELAY_{{ p.0 }}/1’,’GOTO_PRE_{{ p.0 }}/1’); keywordstylekeywordstyle keywordstylekeywordstyle set_param(’untitled/FROM_{{ loop.index }}’,’position’, [{{ 200 + 400 * loop.index0 keywordstylekeywordstyle}}, 140, {{ 200 + 400 * loop.index0 + 40 }}, 180]); keywordstylekeywordstyleset_param(’untitled/DELAY_{{ p.0 }}’,’position’, [{{ 200 + 400 * loop.index0 + 140 keywordstylekeywordstyle}}, 140, {{ 200 + 400 * loop.index0 + 180 }}, 180]); keywordstylekeywordstyleset_param(’untitled/GOTO_PRE_{{ p.0 }}’,’position’, [{{ 200 + 400 * loop.index0 + keywordstylekeywordstyle280 }}, 140, {{ 200 + 400 * loop.index0 + 320 }}, 180]); keywordstylekeywordstyle keywordstylekeywordstyleset_param(’untitled/FROM_{{ loop.index }}’,’GotoTag’,’{{ p.0 }}’) keywordstylekeywordstyleset_param(’untitled/GOTO_PRE_{{ p.0 }}’,’GotoTag’,’PRE_{{ p.0 }}’) keywordstylekeywordstyle{% endfor %} keywordstyle keywordstyle We now proceed to build the previous layer of the monitor. This layer has a set of blocks for each signal that refer to previous states of the system. Each set of blocks consists of aFrom block to obtain the signal value from the previous layer, a Delay block to delay this value a parameterised number of states, and a Goto block to make it accessible throughout the rest of the model as in the previous layer. keywordstyle keywordstyle keywordstylekeywordstyle {% for id, expr in exprs.items() %} keywordstylekeywordstyleprop = Stateflow.Data(ch); keywordstylekeywordstyleprop.Name = ’{{ id }}’; keywordstylekeywordstyleprop.DataType = ’boolean’; keywordstylekeywordstyleprop.Scope = ’Input’; keywordstylekeywordstyle keywordstylekeywordstyle{% set outer_loop = loop %} keywordstylekeywordstyle keywordstylekeywordstyleadd_block(’simulink/User-Defined Functions/MATLAB Function’,’untitled/{{ id }}’); keywordstylekeywordstyleset_param(’untitled/{{ id }}’,’position’, [800, {{ 450 + 100 * loop.index0 }}, 900, keywordstylekeywordstyle{{ 450 + 100 * loop.index0 + 50 }}]); keywordstylekeywordstyleadd_line(’untitled’,’{{ id }}/1’,’Chart/{{ loop.index }}’); keywordstylekeywordstyle keywordstylekeywordstylefHandle = rt.find(’-isa’,’Stateflow.EMChart’,’Path’,’untitled/{{ id }}’); keywordstylekeywordstylefHandle.Script = sprintf([’function {{ id }} = fcn({{ expr.2 }})\n’,’{{ id }} = {{ keywordstylekeywordstyleexpr.0 }};’]); keywordstylekeywordstyle keywordstylekeywordstyle{% for arg in expr.1 %} 4.1. Runtime verification with monitors 31 keywordstylekeywordstyle{% set index = outer_loop.index0 + loop.index0 %} keywordstylekeywordstyle keywordstylekeywordstyleadd_block(’simulink/Signal Routing/From’,’untitled/FROM_{{ id }}_{{ loop.index }}’) keywordstylekeywordstyleset_param(’untitled/FROM_{{ id }}_{{ loop.index }}’,’position’, [600, {{ 450 + 100 keywordstylekeywordstyle* index }}, 650, {{ 450 + 100 * index + 50 }}]); keywordstylekeywordstyle set_param(’untitled/FROM_{{ id }}_{{ loop.index }}’,’GotoTag’,’{{ arg }}’) keywordstylekeywordstyleadd_line(’untitled’,’FROM_{{ id }}_{{ loop.index }}/1’,’{{ id }}/{{ loop.index }}’ keywordstylekeywordstyle); keywordstylekeywordstyle{% endfor %} keywordstylekeywordstyle keywordstylekeywordstyle{% endfor %} keywordstyle keywordstyle The next layer being built is the mathematical layer. It consists of two loops: the first generates a MATLAB function for each mathematical expression that appears in the specification so that it can be evaluated; the inner loop goes through the function inputs and generate From blocks to access the respective signal value that corresponds to each input. All functions output boolean values that are connected to the Stateflow block. These values are interpreted as the propositional variables of the formulas. keywordstyle keywordstyle keywordstylekeywordstyle {% for const in constants %} keywordstylekeywordstyle{{ const }} = {{ loop.index }}; keywordstylekeywordstyle{% endfor %} keywordstylekeywordstyle keywordstylekeywordstyle{{ stateflow }} keywordstylekeywordstyle keywordstylekeywordstylesfsave(’untitled’,’{{ new_name }}’); keywordstyle keywordstyle Finally, we define the necessary constants that were used in the formula. We render the Stateflow block, which was generated by a subclass of this abstraction according to the verification algorithm it encodes. The chart is saved with the given name. 4.1.1Deterministic Finite Automaton A deterministic state automaton (DFA) is a transition system equipped with a set of accepting states. By providing a string of input symbols and checking if the last input symbol 4.1. Runtime verification with monitors 32 leads into an accepting state, we verify that the string is a valid computation for that transition system. Figure 12: Example of a deterministic finite automaton. Figure 12 demonstrates an example of a DFA for the property Every time p holds, q holds in the next step. The DFA has an initial state 1and an accepting state 3. If the execution trace leads the DFA into the accepting state, the system will be trapped in that state and the property will be considered violated. An example of a trace that violates this property is {p},{p, q},{}. In the first input symbol pholds and therefore qmust hold in the next input symbol, which leads the system into transitioning to state 2. State 2expects qto hold, otherwise it transitions to state 3, meaning that the property was violated. In the next input symbol, qholds and so does p, so the system will wait again for qto happen and thus remain in state 2. Finally, in the last input symbol, qdoes not hold and the system evolves into state 3. The system remains trapped in state 3and the monitor reports that the property was violated. Stateflow is the feature provided by Simulink to introduce deterministic finite automatons in a Simulink model. If we know how to transform the formula into a DFA, checking if the accepting state is reachable within a DFA is the default algorithm we use. That is the case for formulas with LTL semantics and SpeAR patterns which, while having Past LTL semantics, have a fixed and well known translation into a DFA. In the case of SpeAR formulas we rely on the recursive semantics of Past LTL to verify the validity of a property. The DFA module is a simple one that extends the monitor abstraction with the data required to describe a DFA, and takes on the task of generating a Stateflow block that describes the respective DFA. The following is a template of the MATLAB script that renders a deterministic finite automaton in Simulink. keywordstyle keywordstyle keywordstylekeywordstyle {% for s in states|sort %} keywordstylekeywordstyleq_{{ s }} = Stateflow.State(ch); keywordstylekeywordstyleq_{{ s }}.Name = ’q_{{ s }}’; keywordstylekeywordstyle{% endfor %} keywordstylekeywordstyle keywordstylekeywordstyleentry = Stateflow.Transition(ch); keywordstylekeywordstyleentry.Destination = q_{{ initial_state }}; 4.2. From a specification language to a monitor 39 if param1then param2param1→param2 if param1then param2else param3param1→param2∧ ¬param1→param3 while param1then param2param1→param2 before param1¬(once param1) never param1historically ¬param1 param1equivalent to param2param1→param2∧param2→param1 Table 1: Examples of desugaring complex SpeAR constructs. Once the pattern is normalised, we proceed to desugar complex constructs such as while and never operators into a set of simpler operators. Figure 4.3demonstrates the initial transformations the specification described in a) goes through. It is converted to prefix form in b) and in cthe previously operator is normalised while the more complex if operator is desugared into a logical consequence. Now that the formulas are in their simplest version, we are able to starting analysing them in order to extract all the necessary data required by the PastFormula abstraction which will render the entire monitor, including the verification logic associated with the recursive semantics of past LTL. The core of this step is the analysis we do on the mathematical expressions, gathering metadata such as the constants, variables, references to values on previous states, and the mathematical expressions themselves. Once this analysis is complete, we replace the mathematical expressions, which are evaluated separately, by propositional variables that assume the value of the evaluated mathematical expression in the current state. This analysis step is recursive over the mathematical expression, descending gradually sub expressions tree. To identify variables and constants we rely on regular expressions, once we reached the roots of the sub expressions tree, and use the convention we specified earlier: variables are lower case, while constants are upper case. For each match we find, we add it either to the variables set or the constants set. If any of the sub expressions includes a previous operator, which is the only temporal operator that can appear inside a mathematical expression, we replace such expression by a new identifier of type PRE signal name. These identifiers are added both to the set of variables and the set of previous values. The math expressions themselves are transformed back into the form, so that they are ready to be evaluated as a MATLAB expression. For every relational expression, we generate an unique identifier and add the expression to the mathematical expressions set. Inside the temporal formula, the expression is replaced by its identifier, assuming the purpose of propositional variable. All this analysis logic is done by the SpearFormula module, which is an extension of PastFormula abstraction. With this analysis we obtain all the necessary metadata to build the Simulink monitor. 4.2. From a specification language to a monitor 40 Listing 4.4demonstrates the results of applying the processes described above to a SpeAR specification. The if condition was transformed into a logic consequence and the mathematical expression no longer appears in the temporal formula, which is now in prefix notation. All the metadata necessary to build the monitor was also collected successfully. keywordstyle keywordstyle keywordstylekeywordstyle Original SpeAR specification: keywordstylekeywordstyleH (if p > MAX_VOLTAGE then previously q) keywordstylekeywordstyle keywordstylekeywordstyleTemporal formula after analysis: keywordstylekeywordstyleH [-> m1 PRE_q] keywordstylekeywordstyle keywordstylekeywordstyleMetadata collected: keywordstylekeywordstyleVariables: {p, q, PRE_q} keywordstylekeywordstylePrevious: {PRE_q} keywordstylekeywordstyleConstants: {MAX_VOLTAGE} keywordstylekeywordstyleMathematical expressions: {m1: p > MAX_VOLTAGE, m2: PRE_q} keywordstyle keywordstyle Listing 4.4: Example of the analysis of a SpeAR specification and the transformations it is subject to. That said, patterns are handled in a different manner. If we identify that abstract syntax tree of a SpeAR constraints corresponds to a pattern, it goes through the same process of metadata extracting. However, each pattern has a well known transformation into a deterministic finite automaton, so SpeAR patterns rely on a DFA instead of the recursive semantics of past LTL. Different instantiations of the same pattern vary only on the metadata: the variables set, the previous set and the mathematical set. From this step onward, all the formulas (either free formulas or patterns) are an extension of the monitor abstraction and thus the MATLAB scripts can be rendered. 4.2.2SALT SALT provides a compiler and thus it is not necessary for us to handle the parsing logic by ourselves. The compiler supports multiple options for its output syntax, such as SMV syntax or SPIN syntax – both well known LTL model checkers. Although none of its options suit us, it still provides us the option to extend the compiler with our own plugins, which allows us to customise its output. SALT can output formulas either in LTL or Past LTL depending on the operators that were used in the SALT formal specification. While we need the resulting LTL formulas in their canonical form, our backend for Past LTL expects formulas in a prefix notation, which is an issue that is simpler to approach while we still have knowledge about the AST of the formula. Thus, we chose to write a plugin for SALT instead of building another parser and transforming the formulas on our backend. 4.2. From a specification language to a monitor 41 In short, the SALT compiler receives SALT specifications as input and will output either canonical LTL, or Past LTL in prefix form. Our tool distinguishes the format being outputted by first trying to interpret the past formulas and, if this fails, handles it as a future formula. When our backend successfully parses a Past Formula from the SALT compiler it instantiates it as PSaltFormula, an extension over the PastFormula abstraction. Similarly to the SpearFormula, this mainly deals with the extraction of metadata, and replacement of mathematical expressions by propositional variables. Remember that mathematical expressions are built upon the quoted propositions that allow for arbitrary text inside a formula. Thus, we can not rely on the abstract syntax tree as we did for SpeAR. Instead, we gradually consume the text while looking for specific patterns: variables, constants, the previous operator, mathematical operators and number literals. We build a new expression by appending every match exactly as it was found on the original expression, except for the previous operator in which case we generate a new identifier and add it in place of the original match. This new expression is added to the set of mathematical expressions that forms the metadata as well as all the variables, constants and previous operators that we were able to match. In the case of LTL formulas we need to transform them into its equivalent DFA. For this task we rely on a project, named Spot (Duret-Lutz et al.,2016), that provides a tool to translate LTL formulas into their respective DFA representation. This tool outputs the DFA as a Hanoi Omega Automata which we parse and then convert into a FSaltFormula, the extension of the DFA abstraction for SALT. keywordstyle keywordstyle keywordstylekeywordstyle HOA: v1 keywordstylekeywordstylename: "G(!a | Fb)" keywordstylekeywordstyleStates: 2 keywordstylekeywordstyleStart: 0 keywordstylekeywordstyleAP: 2 "a" "b" keywordstylekeywordstyleacc-name: Buchi keywordstylekeywordstyleAcceptance: 1 Inf(0) keywordstylekeywordstyleproperties: trans-labels explicit-labels state-acc complete keywordstylekeywordstyleproperties: deterministic stutter-invariant keywordstylekeywordstyle--BODY-- keywordstylekeywordstyleState: 0 {0} keywordstylekeywordstyle[!0 | 1] 0 keywordstylekeywordstyle[0&!1] 1 keywordstylekeywordstyleState: 1 keywordstylekeywordstyle[1] 0 keywordstylekeywordstyle[!1] 1 keywordstylekeywordstyle--END-- 4.3. Extraction DSL 42 keywordstyle keywordstyle Listing 4.5: Example of a DFA in the Hanoi Omega Automata representation. Listing 4.5shows the output of the tool for the temporal formula G (a →F b). The HOA representation starts by stating some metadata about the DFA such as: 1. the initial state 0in the field Start. 2. the number of atomic propositions and their respective identifiers in the field AP. 3. the number of acceptance states, their respective id and some other properties in the field Acceptance. The metadata is followed by the DFA itself, by stating all states and all transitions as well as the conditions that enable such transitions. In our case, all atomic propositions correspond to mathematical expressions from which we need to follow the usual procedure of metadata extraction, and then replacing them by simple propositional variables that map into their evaluation at runtime. From this step onward both future and past formal constraints are an extension of the monitor abstraction, and thus we are ready to render their respective MATLAB scripts that generate the equivalent monitor. 4.3 extraction dsl The extraction DSL is based on parser combinators, high-level functions that receive parsers as arguments and return a new parser, allowing us to define more complex parsers by combining simpler parsers. The modifiable pattern, for instance, builds upon the modifier and pattern parsers. modi f iable pattern =optional(modi f ier),pattern Each parser encodes a regex construction and this allow us to parse the DSL into a proper regex that can be used to extract requirements. The supported regex features are described below. •Capture groups, which are essential to extract specific pieces of data from the text. •Character classes like digit, lowercase, any char, and many others. •Placement match such as start with, end with •Pattern quantifiers such as zero or more,one or more and optional or numbered patterns. 4.4. Final results 43 •Range quantifiers such as between,up to and at least. •Sequences of possible patterns that can be matched, encoded as one of. •pattern negation,start of string and end of string expressions. •Support for actual regex patterns and custom extractors that can be reused as patterns. While Table 2shows simple translation rules that are performed by the parsers, there are more complex translation rules such as the modifiable pattern. This parser starts by compiling the pattern and, if there is a modifier, applies the modifier to the result. The compilation process is aware of its environment so that the user can rely on previously defined extractors to build new ones on top of them. followed by expr expr starts with expr bexpr ends with expr expr$ Table 2: Translation rules performed by parsers. 4.4 final results In this section we intend to do an overview of our workflow, this time focusing on the transformations the formal specifications go through instead of how they are performed. Consider the extractor described in Listing 3.2that compiles down to (REQ [0−9]+) :\s∗(.+)\n{2} and with which we are able extract the requirements we saw previously in Listing 3.1. From these requirements, we are interested in the first two: keywordstyle keywordstyle keywordstylekeywordstyle REQ_1: When the system is in state_1 and signal_3 + signal_2 > 100, the system shall keywordstylekeywordstyletransition to state state_3. keywordstylekeywordstyleREQ_2: Once the system is in state_3 occurs, then the system will be in state_4 keywordstylekeywordstylesomewhere in the future. keywordstyle keywordstyle We formalise REQ 1using SALT and REQ 2using SpeAR as previously shown in Listing 3.4and Listing 3.5, respectively. With both formulas formalised, we can trigger the monitor generation process. keywordstyle keywordstyle keywordstylekeywordstyle REQ_1: assert always (if ’state == STATE_3’ then eventually ’state == STATE_4’) 4.4. Final results 44 keywordstylekeywordstyleREQ_2: historically if previously state equal to STATE_1 and signal_3 + signal_2 > keywordstylekeywordstyle100 then state equal to STATE_3 keywordstyle keywordstyle For REQ 1this process starts by invoking the SALT compiler. Since REQ 1is a future formula, the compiler output will be pure LTL which will then be processed by Spot. Finally, we analyse the mathematical expressions to extract all the necessary metadata. The replacement of mathematical expressions by boolean propositions was already handled by Spot, and it is only necessary to readjust the name of boolean proposition to match the identifier we give to the math expressions. Listing 4.6shows the DFA outputted by Spot after adjusting the propositional variables’ names. keywordstyle keywordstyle keywordstylekeywordstyle State: 0 {0} keywordstylekeywordstyle[!expr0 | expr1] 0 keywordstylekeywordstyle[expr0&!expr1] 1 keywordstylekeywordstyleState: 1 keywordstylekeywordstyle[1] 0 keywordstylekeywordstyle[!1] 1 keywordstyle keywordstyle Listing 4.6: Excerpt of Spot output for REQ 1. For REQ 2this means changing it into prefix form, followed by normalising and desugaring its operators, resulting in a temporal formula with just the operators from Past LTL semantics. To finish the processing this formal specification goes through, we extract the mathematical expressions while simultaneously collecting the metadata. Listing 4.7describes the final result. keywordstyle keywordstyle keywordstylekeywordstyle Temporal formula: keywordstylekeywordstyleH [-> [&& m0 m1] m2] keywordstylekeywordstyle keywordstylekeywordstyleMetadata collected: keywordstylekeywordstyleVariables: {PRE_state, signal_3, signal_2} keywordstylekeywordstylePrevious: {PRE_state} keywordstylekeywordstyleConstants: {STATE_1, STATE_3} keywordstylekeywordstyleMathematical expressions: {m0: PRE_state == STATE_1, m1: signal_3 + signal_2 > keywordstylekeywordstyle100, m2: state == STATE_3 keywordstyle keywordstyle Listing 4.7: Resulting data after processing REQ 2. With both requirements processed, we are able to automatically build the runtime monitors. These monitors can then be plugged into the system model and run in parallel with 4.4. Final results 45 it during simulations. By observing the monitor output, the engineer is able to detect if the any of the properties did not hold and act accordingly by either fixing the design or checking the consistency of the requirements. 5 C O N C L U S I O N Critical systems require a high level of confidence in their correctness before they can be deployed. Today, the industry already relies on model-based engineering and simulations to improve the confidence in their designs by doing an early exploration of the behaviour their solution exhibits. The proof of concept described in this dissertation builds upon these processes and, in order to verify the system behaviour, it relies on runtime monitoring instead of typical unit testing. As such, instead of verifying the system by relating pairs of input/output, we focus on verifying its correctness over execution traces, allowing us to state properties that the system must satisfy. Since we automatically generate the monitors from the formalised requirements, the runtime monitors we generate are also checking the design compliance with the elicited requirements. Our workflow is also heavily focused on reducing the obstacles that requirements engineers face when using tools based on formal methods. To achieve this, we chose to support high-level specification languages with a syntax as close to that of natural language as possible. Thus, both SALT and SpeAR specification languages provide expressive operators while not requiring strong formal methods foundations. Furthermore, we do not expect requirements engineers to be versed in writing regular expressions and thus provided a DSL to ease the extraction of requirements. In the end, we were able to successfully generate runtime monitors for the Simulink environment based on SALT and SpeAR specifications. 5.1 future work Currently, our tool limits the flexibility provided by SpeAR and SALT by not supporting the definition of user-defined operators. There are several ways in which we could overcome this limitation, for instance, by supporting a library with operators that the users could contribute to. We also wish to add support for the SALT operators whose semantics are based on Timed LTL. This would allow our tool to support yet another class of properties, i.e. properties with real time constraints. 46 5.1. Future work 47 It would also be interesting to explore the concept of code generation by inspecting the system model and the associated runtime monitors and generating both the application and the executable equivalent of the monitors. Such task would be a challenging one since the monitors would require a low execution overhead in order to keep it from impacting the system. Another problem that would require attention in this approach would be the concurrency between the application and the monitors, which could not impact the correctness of the requirements. This approach would also be interesting to monitor non-functional requirements such as memory consumption or energy available. Such requirements could be follow a similar methodology to the one described in this dissertation but targeting AADL instead of Simulink. B I B L I O G R A P H Y E. Hoffman B. Rodes M. Aiello J. Davis A. Fifarek, L. Wagner. Spear v2.0: Formalized past ltl specification and analysis of requirements. NASA Formal Methods Symposium, May 2017,2017. M. Ahmadian. Model based design and sdr. IET Conference Proceedings, pages 19–19(1), January 2005. URL https://digital-library.theiet.org/content/conferences/10. 1049/ic_20050389. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking, volume 26202649.01 2008. ISBN 978-0-262-02649-9. Howard Barringer, Michael Fisher, Dov Gabbay, Richard Owens, and Mark Reynolds. The imperative future: Principles of executable temporal logic. 01 1996. Ali Behboodian. Model-based design. 2,05 2006. Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, and Laurent Xu. Spot 2.0— a framework for LTL and ω-automata manipulation. In Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA’16), volume 9938 of Lecture Notes in Computer Science, pages 122–129. Springer, October 2016. doi: 10.1007/978-3-319-46520-38. M.B. Dwyer, George Avrunin, and James Corbett. Patterns in property specifications for finite-state verification. pages 411–420,02 1999. doi: 10.1109/ICSE.1999.841031. Andrew Gacek, Andreas Katis, Michael Whalen, John Backes, and Darren Cofer. Towards realizability checking of contracts using theories. 02 2015. doi: 10.1007/ 978-3-319-17524-913. Volker Gruhn and Ralf Laue. Patterns for timed property specifications. Electronic Notes in Theoretical Computer Science,153:117–133,05 2006. doi: 10.1016/j.entcs.2005.10.035. Sascha Konrad and Betty Cheng. Real-time specification patterns. Proceedings - 27th International Conference on Software Engineering, ICSE05, pages 372–381,06 2005. doi: 10.1109/ICSE.2005.1553580. Ron Koymans. Specifying real-time properties with metric temporal logic. Real-Time Systems,2:255–299,11 1990. doi: 10.1007/BF01995674. 48