documentsn.com

1 IntroductionNowadays, software is ubiquitous in mechatronic systems like cars or other vehicles.It realizes the information processing in complex control loops involving sensor andactuator technology. We are faced with the environmental impacts of software interms of comfort functions related to information, entertainment, and safety. Impressive indicators for today’s role of software in automotive systems are numbers like 100electronic control units per car [EZK 13], running one gigabyte of software [PBKS07]with 100 million lines of code [Mös10] in order to provide up to 2000 individual functions [Bro06]. 90 percent of today’s innovations in the automotive industry stem fromelectronics including software [HMG11].Due to the inherent connection of mechatronic systems to real-world physical processes, software systems face hard real-time requirements, i.e. software must react toexternal stimuli within specific time bounds. Along with the exponential rise of software in the automotive industry [PBKS07], the consequences of unsatisfied real-timerequirements tend to be increasingly drastic. To avoid costs from contractual penalties,or even loss of human life, safety-critical computer systems require the guaranteed absence of errors in the software they are running [Sto96]. A plain testing of systemsunder certain selected conditions is therefore inappropriate in the domain of mechatronics. Instead, there is a pressing need for reliable verification techniques that coverthe entire real-time behavior under all possible conditions.Beside the ongoing trend towards real-time computing, today’s systems are increasingly distributed and networked. An amount of 2500 signals [Alb04] exchangedon top of five bus systems per car [Bro06] gives evidence for the rising importanceof interaction. However, this trend is not limited to single systems, but involvesan increasing information exchange between different autonomous systems for coordination purposes [SW07]. Hence, such networked systems act as systems of systems [Luk98]. Overcoming the dynamic structure of the underlying ad-hoc communication networks, the interaction tends to be carried out by an asynchronous exchangeof discrete messages [SS11], controlled by state-based software. As an example, Figure 1.1 illustrates the approach of vehicle-to-vehicle communication for an increasedsafety in overtaking situations. Safe overtaking is always limited in time and thereforeinvolves hard real-time requirements. Coordination over message exchange protocolscan prevent a sudden acceleration of an overtaken vehicle, alleviating a serious safetyhazard.Whereas safety is among the key functions that software addresses in today’s systems, the rising software complexity poses huge challenges with respect to guaranteedsafety. The combination of complex designs and guaranteed safety is a key challenge tomechatronic systems and requires consideration at an early stage of the development1

1. IntroductionFigure 1.1: Vehicle-to-Vehicle Communication in an Overtaking Scenarioprocess. Model-driven design [Sch06] is a promising approach towards this combination. Relying on reusable models as abstract domain-specific design elements, themanageability of the overall design improves drastically. In addition, due to the formal characteristics of models, formal verification techniques are applicable to provethe compliance with specific requirements. Model checking [CGP00] is a prominentformal verification technique that operates on the model level, exhaustively hedginga system against corner case design errors.To enable formal verification techniques like model checking and improve the overall design manageability, the MechatronicUML design method [EHH 13; BBB 12]proposes a model-driven approach to the construction of networked mechatronic systems. MechatronicUML provides modeling support for component-based softwaresystems [Szy98] involving real-time coordination behavior. Figure 1.2 shows twoMechatronicUML component instances representing networked vehicles. Connectedfor message exchange, the component ports specify a real-time coordination behaviorthat implements a dedicated message exchange protocol for safe overtaking scenarios. The state-based port behavior is specified using so called Real-Time Statecharts,a combination of state machines [OMG11c] provided by the Unified Modeling Language (UML) and timed automata [AD90]. The Real-Time Statecharts ensure that theovertaken front vehicle refrains from acceleration during overtaking by the rear vehicle. Along with this crucial safety challenge, the protocol also faces the requirementsof deadlock freedom and to properly enable the overtaking. Figure 1.2 also illustratesthese requirements in terms of formalized properties attached to the coordination protocol.1.1 ProblemExisting tool-support for model checking is nowadays limited to general-purpose specification techniques for the system under consideration, relying on low-level modeling formalisms. The result is a significant semantic gap between domain-specific languages like MechatronicUML on the one hand, and verification formalisms on theother hand. For instance, concepts like the hierarchical composition of componentsand the asynchronous exchange of messages are unknown to most verification formalisms. To bridge the semantic gap, engineers are required to leave familiar domainconcepts behind and bother with low-level verification formalisms to encode system2

1.1 ProblemA[] not deadlockA[] rear.overtaking implies front.noAccelerationE rear.overtaking:Overtaking:rear:frontv2 : Vehiclev1 : VehiclerearfrontFigure 1.2: MechatronicUML Component Instance Configurationbehavior manually. The results are drawbacks like the huge manual effort in combination with increased development times, and also the possibility for undetecteddeficiencies resulting from an erroneous encoding of the system behavior.Beside the crucial task of proving the absence of errors, model checking tools alsoaim at providing diagnostic user feedback along with the identification of an existingerror. The diagnostics usually comprise a counter-example of the system behaviorwith respect to the verified requirement. Obviously, presented counter-examples arebased on the underlying verification formalism and are therefore of little avail for domain engineers. Even if an engineer successfully bridges the semantic gap from thedomain-specific language to the verification formalism, he is likely to stumble over theadditional challenge of interpreting the counter-example against the original domainspecific design model. This manual interpretation is not only complex but error-prone,and therefore still suffers from problems like increased development times or undetected design deficiencies.As a remedy to the problematic integration of domain-specific modeling and formal verification, in the year 2004, Hirsch [Hir04] connected Real-Time Statecharts tothe Uppaal1 tool environment [BLL 96] by prototyping an automatic transformation.Uppaal is a state-of-the-art model checker that enables formal verification for systems affected by real-time requirements. Apart from incompatibility problems withevolved MechatronicUML versions, the transformation lacks important conceptslike quality-of-service assumptions with respect to the asynchronous interaction, likemessage delay or loss. Hence, a vast range of real-world circumstances remains unconsidered by this verification approach. As another major disadvantage, the approachis restricted to the connection from domain-specific models to verification formalism,but puts the burden of interpreting counter-examples into the opposite direction onthe domain engineer. Hence, the diagnostic capabilities of the Uppaal integration byHirsch [Hir04] face serious limitations with respect to the cause study for counterexamples.1http://www.uppaal.com3

1. Introduction1.2 ObjectiveThe objective of this thesis is to integrate the Uppaal model checker with MechatronicUML in a transparent way. Transparency refers to the option for MechatronicUML domain engineers to remain unaware of the formal verification details,still obtaining accurate and meaningful verification results including counter-examples.We focus on redesigning the transformation approach by Hirsch [Hir04] for today’sstate of the MechatronicUML design method. In addition, we explicitly address thepresentation of counter-examples at the MechatronicUML level, saving domain engineers from the need for a manual interpretation of formal verification details againstdomain-specific concepts. We therefore alleviate the necessity to make contact withthe underlying verification formalism at all, and therefore prevent engineers from theneed to understand how the formalism relates to domain-specific concepts.A well-structured evaluation will enable conclusions with respect to the goal of semantics preservation for our connections between MechatronicUML and Uppaal.By improving the analyzability of MechatronicUML-based models on top of a transparent Uppaal model checking, the overall goal of this thesis is to promote the maturity of end products in the context of the MechatronicUML design method.1.3 ApproachThis thesis tackles the problems described in Section 1.1 by enabling Uppaal-basedmodel checking for MechatronicUML in a transparent way. Similar to Hirsch [Hir04],we aim at a model transformation that automatically converts MechatronicUMLbased system models to a format suitable for offhand verification by Uppaal, as depicted in Figure 1.3. A transparent integration of Uppaal into MechatronicUML requires a certain accuracy of the verification results, i.e. the transformation should preserve the semantics of the initial MechatronicUML-based design model. The seamless Uppaal interoperability will comprise a chain of numerous transformation steps,conceptually aligning the formalisms step by step.The transformation from MechatronicUML towards Uppaal gives rise to an automatic model checking. Counter-examples generated by Uppaal have the form ofa trace, i.e. a sequence of behavioral runtime snapshots towards the violation of aspecified requirement. In order to establish transparency of the verification from theviewpoint of MechatronicUML domain engineers, our approach is to align the traceswith the original MechatronicUML language elements. We therefore introduce asecond transformation for traces back towards MechatronicUML, as also shown inFigure 1.3. We address this transformation challenge by resolving Uppaal-specifictrace elements towards their corresponding MechatronicUML elements in the original design model, generating a trace representation which is familiar to the domainengineer. As an obvious prerequisite for this strategy, we have to ensure traceabilityof the initial transformation from MechatronicUML towards Uppaal.4

1.4 StructureSystem ModelCounter-Example TraceFigure 1.3: Transformation Approach between MechatronicUML and UppaalWe will obtain meaningful conclusions from our approach by systematically evaluating the semantics preservation, which is a key aspect for the construction of theentire transformation approach. We refer to a standardized and well-understood evaluation technique in the field of software engineering in terms of the Goal QuestionMetric (GQM) approach [BW84]. Due to its well-defined composition and field-testedconcepts, GQM appears to be suitable for the delivery of meaningful evaluation results, based on a systematic refinement of the relevant aspects. The evaluation willconcentrate on representative MechatronicUML-based test models.1.4 StructureThe remainder of this thesis is structured as follows: Section 2 describes fundamentalbasics in terms of the underlying model-driven software development approach, realtime verification concepts, the MechatronicUML design method, and GQM-basedevaluation. In Section 3, we study related work with respect to other transformationstowards the Uppaal model checker, transformations from MechatronicUML to otherverification or simulation formalisms, and also existing verification approaches addressing transparency. Section 4 describes our transformation approach from MechatronicUML towards Uppaal, whereas in Section 5, we address the challenge of resolving Uppaal traces back to the MechatronicUML level. Our implementation approachis subject to Section 6, before presenting the evaluation results in Section 7. Finally,we give concluding remarks and address topics left for future work in Section 8.5

2 BasicsThis section introduces fundamental basics which are relevant in the scope of thisthesis. As our basic engineering paradigm, we describe the model-driven softwaredevelopment approach in Section 2.1. Section 2.2 introduces timed automata as a basic modeling formalism. In Section 2.3, we address the formalization of real-time requirements. Based on the above formalisms, we capture the approach of timed modelchecking in Section 2.4. The MechatronicUML design method is subject to explanation in Section 2.5, whereas the final Section 2.6 captures our Goal Question Metricevaluation method.2.1 Model-Driven Software DevelopmentThe concept of a model [Sta73] refers to an abstract representation of some real-worldentity. Its key concepts are listed below: Abstraction is the approach of creating an entity’s representation in such a way,that it reduces to specific essential attributes, leaving out non-essential attributesof the original. Essentiality of an attribute is not given a priori, but depends on a certain intended task. Despite the abstraction of specific attributes, the pragmatics of amodel with respect to this task must still be given. Pragmatics with respect to a task are ensured by retaining a certain correspondence, i.e. a model must substitute its original under specific conditions.In general, models contribute to the solution of problems. Abstraction enables simplified reasoning about problems and aids the construction of solutions. In order toestablish pragmatics, the correspondence between model and its original must ensurethat the solution obtained from the abstract model is also a valid solution to the original.2.1.1 Model-Based Software DevelopmentFocusing on the domain of software engineering, challenging problems are basicallyconcerned with the construction of software systems. Modeling software systems constitutes a prescriptive [Sta73] approach, since the original system only emerges fromits abstract representation. We refer to the following definition with respect to therole of models in software engineering:7

2. BasicsDefinition 2.1 (Model) “A model is an abstract representation of a system’s structure,function or behavior” [SV06, p. 18].Abstraction actually has a long tradition in software engineering, since new technologies tend to abstract from the complexity of preliminary ones. In the presence ofabstraction, the problem of software construction merely corresponds to transforming an abstract software specification into a concrete software system running on aspecific platform. A platform provides specific computing capabilities as a foundationfor concrete software systems. As opposed to models, that basically serve for problemdescription, a platform is said to reside “in the solution space” [SV06, p. 59]. The application of the model concepts to software engineering led to the notion of model-basedsoftware development. An application implies some solution strategy to transforman abstract model into a concrete software system. Nowadays, the UML family of diagram types [OMG11c] forms the basis of most model-based software developmentapproaches.2.1.2 AutomatizationCombining model concepts with computing is quite obvious, since computers allowreasoning to be automatized. Automatization gives rise to reuse of existing solutionstrategies, i.e. enables the automatic construction of solutions to specific problems.In particular, this pertains to the transformation task from an abstract model to aconcrete software system mentioned in Section 2.1.1. New technologies often stillrely on the proven effectiveness of their predecessors by automatically transformingabstract specifications into more concrete specifications of software systems. Consequently, we identify automatization as a key principle of model-driven software development, as opposed to approaches termed model-based. Connected to a certainplatform by means of an automatic transformations, a model acts as “central artifact” [SV06, p. 79] in model-driven software development.2.1.3 Domain-Specific LanguagesBeside the automatization aspect, approaches termed model-driven differ from modelbased techniques by a shift in the underlying domain.Definition 2.2 (Domain) A domain is “a bounded field of interest or knowledge” [SV06,p. 56].Paradigms like high-level programming languages or UML [OMG11c] are still closelylinked to the domain of computing as such. Although the aforementioned approachesprovide software solutions for a wide range of application domains, responsible engineers are restricted to general-purpose specification techniques. We refer to thechallenge of expressing domain concepts adequately by means of general-purpose languages as semantic gap.8

2.1 Model-Driven Software DevelopmentIn contrast, model-driven software development [SV06] focuses on the use of domainspecific languages for the specification of software systems. Hence, transformationsproduce concrete software solutions from domain-specific models and thus bridge thesemantic gap. Schmidt [Sch06] describes the use of domain-specific modeling languages in combination with transformation engines and generators as key aspects ofmodel-driven software development.Domain-specific languages enable the explicit specification of abstract solution strategies developed by domain experts, and also reuse of these strategies via automatictransformations. By bridging the semantic gap between specific domains on the onehand, and computing platforms on the other hand, the usage of domain-specific languages constitutes another key principle in model-driven software development.2.1.4 Meta-ModelingIn order to automatize transformations by means of computers, the specifications tobe transformed must be machine-readable, i.e. formal with respect to some metaspecification. Relying on models, meta-modeling describes the approach of providingthe meta-specification for models in terms of another model. This so called meta-modelacts as model of a domain, including its elements and construction rules. It definesthe set of valid constructable models as instances of the meta-model, i.e. sentencesof a domain-specific modeling language. Hence, a meta-model gives rise to a typeinstance-relationship with models. The essential components of a meta-model are an abstract syntax, defining domain elements and construction rules, and static semantics, giving a meaning to models without considering them in someexecution context1 .In the scope of a domain-specific modeling language, the above meta-model concepts are linked to at least one concrete syntax, defining how to express models in aconcrete manner, and dynamic semantics, charged with semantics definition fotr models during execution.2.1.5 Model TransformationSection 2.1.2 emphasized the essential role of automatic transformations with respectto reuse of existing solution strategies. Stahl and Völter describe the task of transformations as to “map models to the respective next level” [SV06, p. 21] on the way tosome platform. Hence, to solve the problem of transforming models to a platform, it1This definition of static semantics is in accordance with the notes of Harel and Rumpe in [HR04].Stahl and Völter [SV06] put static semantics on a level with additional syntax constraints referredto as “context conditions" [HR04, p. 65]. However, adhering to this definition would lead to theinconsistency that “static semantics belong to the syntax rather than to the semantics of a language” [SV06, p. 58].9

2. Basicsmay also be desirable to engage with existing solution strategies. This approach implies the transformation of models into other models, traversing various intermediatemodeling levels on the way to a platform.Definition 2.3 (Model Transformation) Model transformations “take one or moresource models as input and produce one or more target models as output, while followinga set of transformation rules” [SK03, pp. 42-43].Noteworthy, although the above definition describes n-way transformations [CH06]with an arbitrary number of models on both sides, it also covers the typical case of a1:1 transformation with single source/target models. The most common scenario is anexogenous [MCG05] model transformation which carries out a change in the underlying modeling language, i.e. source and target meta-model differ. Focusing on programtransformation in general, Visser addresses the same concept as translation [Vis01].However,

Due to the inherent connection of mechatronic systems to real-world physical pro-cesses, software systems face hard real-time requirements, i.e. software must react to external stimuli within speci c time bounds. Along with the exponential rise of soft-ware in the automotive in