=Paper=
{{Paper
|id=Vol-1508/paper4
|storemode=property
|title=AutoFOCUS 3: Tooling Concepts for Seamless, Model-based Development of Embedded Systems
|pdfUrl=https://ceur-ws.org/Vol-1508/paper4.pdf
|volume=Vol-1508
|dblpUrl=https://dblp.org/rec/conf/models/AravantinosVTHS15
}}
==AutoFOCUS 3: Tooling Concepts for Seamless, Model-based Development of Embedded Systems==
https://ceur-ws.org/Vol-1508/paper4.pdf
AutoFOCUS 3: Tooling Concepts for Seamless,
Model-based Development of Embedded Systems
Vincent Aravantinos, Sebastian Voss, Sabine Teufl, Florian Hölzl, Bernhard Schätz
fortiss GmbH
Guerickestr. 25
80805 Munich, Germany
Email: hoelzl@fortiss.org
Abstract—This paper presents tooling concepts in AUTO - Since all of these views are projections of the underlying sys-
FOCUS 3 supporting the development of software-intensive tem model, these views are directly integrated. Furthermore,
embedded system design. AUTO FOCUS 3 is a highly integrated linking views allow an additional integration (like the mapping
model-based tool covering the complete development process
from requirements elicitation, deployment, the modelling of the of a component behavior to a hardware element, or a required
hardware platform to code generation. This is achieved thanks partial execution to a completely defined behavior). Besides
to precise static and dynamic semantics based on the FOCUS allowing a manageable precise description of a system under
theory [1]. Models are used for requirements, for the software development, the system model also enables different analysis
architecture (SA), for the hardware platform and for relations and synthesis mechanisms (like the compatibility analysis of a
between those different viewpoints: traces from requirements to
the SA, refinements between SAs, and deployments of the SA to partial and complete behavior or the deployment synthesis of
the platform. This holistic usage of models allows the provision of components to a hardware platform). To support the different
a wide range of analysis and synthesis techniques such as testing, tasks in a development process, the views are furthermore
model checking and deployment and scheduling generation. organized in viewpoints. A viewpoint serves as a construct for
In this paper, we demonstrate how tooling concepts on different managing the artifacts related to the different stakeholders of
steps in the development process look like, based on these
integrated models and implemented in AUTO FOCUS 3. the development process [2, Chapter 3]. The AUTO FOCUS 3
Index Terms—AutoFOCUS3, Seamless MBD, Model-Based viewpoints focus on the definition of the system requirements
Development, Embedded Systems, Tooling Concept, Tool in a requirements analysis, the design of the software as a
network of communicating components in form of a software
I. I NTRODUCTION architecture, and the realization of the system as scheduled
Embedded systems are increasingly developed in a model- tasks executed on networked processors in form of a hardware
based fashion facilitating constructive and analytic quality architecture.
assurance via abstract component-models of the system under The importance of integrated models, views and viewpoints
development. A variety of different tools claim to support a is widely recognized and influenced the definition of many
model-based approach; however, these tools mostly cover cer- methods and frameworks in systems, software and enterprise
tain parts of the development process. In this paper, we demon- engineering [2], [3] and provides the basis for this paper.
strate the advantage of integrated models and provide tooling The objective of AUTO FOCUS 3 is to implement tooling
concepts for various design steps. Both together leverage the concepts which demonstrate that such an approach is indeed
benefits of a seamless model-based approach based on well- feasible through a ready-to-use, open-source implementation
defined semantics. The objective of this paper is to present in a pre-series quality. The current AUTO FOCUS 3 is a
such tooling concepts in an entire tool (AUTO FOCUS 3) revised and improved version of earlier prototypes [4], [5]
in its current advanced feature state, which is open source (the oldest dating back to 1996). Previous papers either report
and freely available at http://af3.fortiss.org. The on particular aspects of the tool [6], [7], [8], [9], or on its use
main contribution of this paper is to demonstrate the seamless in the context of industrial case studies [10], [11], [12]. The
integration of the integrated models. underlying ideas of the current AUTO FOCUS 3 incarnation
AUTO FOCUS 3 is built on a system model based on the FO- are presented in [13].
CUS theory [1] that allows to precisely describe a system, its AUTO FOCUS 3 is not tied to a specific development
interface, behavior, and decomposition in component systems process, but most developments done with AUTO FOCUS 3
on different levels of abstraction. To manage the complexity would typically follow the following process or variations
of describing such a system, different views are used for these thereof:
aspects, providing dedicated description techniques for differ- 1) Requirements Analysis. Requirements are elicited, doc-
ent structural aspects (like the decomposition of a component umented as structured text, organized, analyzed and
in a network of subcomponents, or the hardware platform the refined, and incrementally formalized. Test suites with
system is implemented on) as well as behavioral aspects (like coverage criteria can be generated from high-level spec-
an exemplary execution of a system, or its complete behavior). ifications.
2) Software Architecture. The system is designed with
a component-based language specifying the application
software architecture and behavior of the system. The
design is validated using simulation, testing (which can
come as refinements from high-level generated tests) as
well as formal verification based on model-checking.
3) Hardware Architecture. The software components are
(possibly automatically) deployed on the platform, w.r.t.
certain system requirements. Schedules optimizing one
or more criteria are generated with the help of SMT
solvers.
The code is completely generated out of the previous models,
according to the deployment and chosen schedule. Further-
more, Safety Cases [14], which are documented bodies of
evidence that provide a convincing and valid argument that a
system is adequately safe for a given application in a given
Fig. 1. Example structured requirement
environment, can be modelled. A Safety Case may contain
complex arguments that can be decomposed, corresponding
to modular system artifacts which are generally dependent on
artifacts from different viewpoints.
The paper is organized as follows: Section II presents
briefly the main modelling viewpoints that are offered by
AUTO FOCUS 3 (requirements, software architecture, and
hardware architecture). Section III presents the transversal
viewpoints which facilitate to make the connections between
the main viewpoints and thus yield a seamless integration. We
also present the benefits resulting of this integration: formal Fig. 2. Message sequence charts
analysis and verification, scheduling, hardware-specific code
generation. Section IV presents related work.
As shown in Fig. 3, AUTO FOCUS 3 provides user-friendly
II. M ODEL - BASED T OOLING C ONCEPTS IN THE templates (see also [15]) to specify temporal logic expressions.
D EVELOPMENT P ROCESS
In this section we present shortly the three modelling
viewpoints supporting the process mentioned in the previous Fig. 3. Temporal logic expression
section.
Once the requirements analysis is sufficiently advanced, it
A. Requirements is possible to express formalized behaviors, e.g., in the form
In AUTO FOCUS 3, requirements are specified model- of state automata. A state automaton typically covers a set of
based: requirements are not just documented as plain text; requirements rather than a single requirement.
the tool provides templates with named fields to define, for
instance, the title of a requirement, its author, a description, a
potential rationale or a review status (see Fig. 1).
Furthermore, requirement sources and glossaries can be
defined. Whenever they are referenced in a textual description
of a requirement, the entries are automatically highlighted and
the definition can be read in a pop-up. Requirements can be
hierarchically grouped by packages and organized by trace
links. Templates for scenarios and interface behavior help to
detail requirements further.
Requirements can not only be documented as text, but also
formalized and represented by machine-processable models.
Message sequence charts (MSC), see Fig. 2, can be used to
describe desired or unwanted interactions of actors.
Temporal logic expressions can be used to express desired
and unwanted behavior of the system under development. Fig. 4. Requirements statistics and reports
Tooling Support. AUTO FOCUS 3 supports the user in
analyzing the requirements, for example through reports on
the review status or statistics (Fig. 4). Simple queries on the
requirements identify for example empty fields, duplicates and
inconsistent status of requirements and their trace links. A
report can be generated from AUTO FOCUS 3 that can be
used for the validation of the requirements by the stakeholders
of the system under development. State automata can be
simulated; this is typically used in both the analysis and Fig. 8. Components and channels
validation of requirements.
B. Software Architecture Finally, components can be decomposed into sub-
The software architecture of a system under development components to allow a hierarchically structured architecture.
can be described using a classical component-based language Tooling Support. Due to the executable formal semantics
with a formal (execution) semantics based on the FOCUS of the component-based modeling language, AUTO FOCUS 3
theory [1]: components execute in parallel according to a facilitates the simulation of the software architecture at all
global, synchronous, and discrete time clock. levels, of a single state automaton (Fig. 9) as well as of
composite components (Fig. 10) providing Model-in-the-Loop
simulations. Test cases can be created and simulated (Fig. 11).
Fig. 5. State automaton
Fig. 9. Simulation of state automata
The behavior of atomic components can be defined by state
automata (Fig. 5), tables (Fig. 6) or simple imperative code
(Fig. 7). Components interact with each other through typed
input and output ports which are connected by fixed channels
(Fig. 8).
Fig. 6. Table
Fig. 10. Simulation of composite components
Furthermore, formal analyses like reachability analysis (see
Fig. 12), non-determinism check, variable bounds checking
and the verification of temporal logic patterns (see Fig. 13)
are available: due to the formal semantics of FOCUS, AUTO -
FOCUS 3 can embed a precise translation of the software
architecture into the language of the NuSMV/nuXmv [16]
model checker. Note that this is all done in a complete
Fig. 7. Simple imperative code transparent way: the translation and call to the model checker
are all done in the background to provide user-friendliness
Fig. 11. Test suites
Fig. 15. Hardware architecture for multicore, with shared memory
workflow. The results of the model checker, namely their
counterexamples, are also translated back in the same way which encompasses execution environments from bare metal
e.g., a counter example to a temporal logic property can be hardware (e.g., chips and wires) over operating system envi-
graphically simulated. ronments up to higher-level runtime environments (e.g., Java
virtual machine with remote method invocation mechanism).
For instance, the aforementioned hardware model for FIBEX
comes also with an implementation for the Flexray protocol
([17]), a time-triggered communication protocol in the auto-
motive domain.
III. S EAMLESS I NTEGRATION
An integration of all of the previously mentioned viewpoints
in an integrated model, resp. tooling environment is an impor-
tant asset for the user: it avoids the effort to integrate tools,
defining their interfaces and dealing with conflicting, missing,
Fig. 12. Unreachable state
or badly documented tool-interfaces, semantics and standards.
However, if these viewpoints remain completely independent
or if the dependency between them remains informal as it is
the case with most existing tools, then only very few benefits
Fig. 13. Verification result
result from its integration. Instead, AUTO FOCUS 3 allows for
model integration leading to a consistent, integrated system
C. Hardware Architecture design. In the following, we present these models as well as
AUTO FOCUS 3 allows to model the hardware: processors analysis and synthesis techniques that demonstrate the benefits
(or, in the automotive domain, ECUs – Engine Control Units), of AUTO FOCUS 3 resulting from this strong integration.
buses, actuators and sensors can explicitly be modeled as
A. Tracing Requirements to the Software Architecture
well as their connections (Fig. 14). Multi-core platforms with
Traces. The integration of requirements (Section II-A) and
the software architecture (Section II-B) can be achieved in
various ways. A first simple integration is the use of informal
traces: for each requirement, traces to components of the
software architecture can be added (see Fig. 16). These traces
Fig. 14. Hardware architecture for generic ECUs
Fig. 16. Traces to the software architecture
shared memory are available (Fig. 15), as well as specific
domain specific hardware e.g., a pacemaker platform was built indicate that the component(s) linked to the requirement shall
specifically for building and deploying models of a pace- fulfill the requirement. Such traces are automatically visible
maker. Similarly, automotive-specific hardware is supported (and navigable) at the level of the component architecture (Fig.
via FIBEX import/export (an XML-based standardized format 17). These traces can be used to display information to the
used for representing TDMA-networks). user. For example, a global visualization of the traces, both
Hardware architecture models actually deal with more than between requirements and between requirements and elements
just hardware: they typically include a platform architecture of the software architecture, is available and allows the user
Fig. 17. Traces, seen from the software architecture
to have an overall picture of the intra- and inter-viewpoint
relations (Fig. 18).
Fig. 18. Traces visualization Fig. 20. Connecting MSCs to components
Refinements. Traces provide informal connections between holds for the messages which can be connected to ports of the
model elements, which is to be expected since most require- corresponding components.
ments are (at least at first, or partly) informal. However, as Once these connections are provided, AUTO FOCUS 3
explained in Section II-A, requirements elicitation can go far allows to verify, by translating the MSC into a temporal logic
enough that a formalized behavior is obtained, e.g., that a formula and by using model checking (in the style of [20]),
state automaton is given. In such cases, traces to the software that the given MSC is indeed feasible in the software architec-
architecture can be enhanced into refinements describing not ture with the referenced components and ports. When feasible,
only a mere connection, but even expressing a formal relation the resulting run can be simulated in AUTO FOCUS 3.
between the requirements-level behavior description and a
software-level implementation of it. A refinement is simply B. Deployment of the Software Architecture on the Platform
defined by expressing how values at the requirement level Deployment of Software to Hardware Components. The
shall be transformed into values at the software level and integration of the software (Section II-B) and hardware archi-
vice versa (Fig. 19). Such refinements can then be used tecture (Section II-C) is done by using deployment models that
describe the integration between different viewpoints. Such
deployments map components from the software viewpoint to
the hardware viewpoint. Furthermore, the deployment model
not only contains the mapping of components but also the
allocation of logical ports of a software component to their
corresponding hardware “ports”, namely hardware sensors for
Fig. 19. Refinement definition sensor values and hardware actuators for actuator outputs.
Fig. 21 illustrates this deployment. Note that the hierarchical
to automatically derive implementation-level test suites from structure of components makes it impossible to have such a
requirements-level ones [18], [19] (which can be automatically simple GUI for deployments in AUTO FOCUS 3, making the
generated according to some coverage criteria) or to verify actual interface different than the one presented in this figure.
by model checking that a component indeed implements a Design Space Exploration for Model Synthesis. Once a
functionality. deployment is defined, Design Space Exploration methods can
Connecting MSCs to the Software Architecture. MSCs be applied to define the scheduling of the software components
can be used in requirements in a semi-formal setting, i.e., the on their respective hardware components. AUTO FOCUS 3
MSC entities represent actors identified in the requirements. provides support to achieve this step by automated synthesis.
Or they can be used in a completely formal setting: when Actually, even deployments can be automatically synthesized
the requirement elicitation is advanced enough, MSC entities as well as complete hardware architectures, according to vari-
can refer to components and the messages between entities ous system requirements, e.g. timing, safety, etc. To do so we
can denote signals exchanged through channels. This can be use Design Space Exploration (DSE) techniques. In [21], we
expressed directly in the MSC editor, e.g., Fig. 20 shows demonstrate how such a joint generation of deployments and
how the properties of an MSC entity named “Merge Entity” schedules can be efficiently done for shared-memory multicore
refers to a component named “MergeComponent”. The same architectures. Each solution of such a synthesis process already
formalization encoding the deployment synthesis as a satisfia-
bility problem over Boolean formulas and linear arithmetic
constraints. A state-of-the-art satisfiability modulo theories
(SMT) solver, namely Z3 [22], is used to compute these
solutions. Using Design Space Exploration techniques during
system development involves the software engineer/designer
itself. The system designer is often not just interested in an
automatically synthesized solution, but even more in various
solutions that can be compared. Therefore, visualization tech-
niques [23] are part of a Design Space Exploration approach
that leverages to guide the system designer through the solu-
tion space.
Furthermore, we propose a tooling concept that includes
a Design Space Exploration Workflow (Fig. 23) enabling to
use intermediate results for next optimization steps, e.g. a
Generated Deployment or a Scheduling Synthesis.
C. Holistic Code Synthesis for Deployed Systems
Fig. 21. Deployment (illustration) Once the software architecture, the platform architecture,
and a (manually defined or automatically synthesized) de-
ployment model are defined, AUTO FOCUS 3 provides the
possibility to have holistic code generation.
Fig. 22. Design Space Exploration results
contains a possible deployment, which in turn already contains
a valid schedule (cf. Fig. ??). This reduces the effort and
complexity in a the workflow for the identification of valid
system designs.
Our approach relies on a symbolic encoding scheme, which
enables to generate the desired models. The symbolic encoding Fig. 24. Generated C code for the deployed system
is done by defining a precedence graph of components based
on the software architecture as a set of tasks and messages The input to the generation facility is the mapping of
and their connections including further information concerning software components to platform execution units. The result
predefined allocations to hardware architecture. of the code generator is a full implementation of the system
model including configuration files for the underlying operat-
ing system as well as bus message catalogs and compile and
build environment configurations (see Fig. 24).
The code generator consists of two parts: the software ar-
chitecture general purpose generator and the platform-specific
target generator. The former translates the different types of
software behavior specifications into an intermediate code
model. From this intermediate representation the final system
Fig. 23. Design Space Exploration Workflow code (see Fig. 25) is generated by the ECU specific code
generator using the ECU target language (e.g. C, Java, VHDL).
The proposed approach has proven to perform in a scalable Note that these specific generators can ignore the intermedi-
fashion for practical sizes ([21]), as it relies on a symbolic ate implementation in cases the original behavior specification
connected to their corresponding system artifacts (e.g., a safety
goal to a requirement from the requirement viewpoint). This –
for instance – enables to automatically guide the construction
of the system architecture w.r.t. the safety claims, as we
demonstrated in [26].
IV. R ELATED W ORK
There are many model-based tools which target the devel-
opment/architecting of embedded systems, but none of them,
Fig. 25. Main loop of the ECU running the Merge component to our knowledge, presents all the features of AUTO FOCUS 3.
Papyrus [27] with Moka1 allows the execution of models
based on the fUML [28] Semantics. Code generation is, as far
can be implemented more efficiently when applying a trans- as we know, only partly implemented, but considering the fast
formation to the target language and/or hardware directly (e.g., growth of Papyrus and Moka, this is should only be a question
a state-less computation component might be implemented of time. A more significant difference to AUTO FOCUS 3
efficiently on a FPGA sub-unit available to the ECU). is that AUTO FOCUS 3 integrates all the modules into a
Every platform integrated in AUTO FOCUS 3 must provide unified software instead of being made of separate modules
its extension to the target generator as well as a justification for diagram editing (Papyrus) and execution semantics (Moka).
that it upholds the semantics of the model of computation This has a significant impact on the verification (either testing
of the software architecture. Likewise, the software code or formal verification): in AUTO FOCUS 3, the semantics for
parts must also be behaviorally equivalent to these formal execution and verification are intrinsically identical; in Papyrus
semantics. Proving such semantic equivalences can be cum- additional work is required to synchronize the semantics of
bersome [24], but is absolutely necessary in order to avoid Moka and the verification tool, for example Diversity2 – a
breaking functional properties established by earlier validation verification tool typically used together with Papyrus.
and verification methods. The widespread commercial tool IBM Rational Rhapsody3
has been offering for a long time a complete tool chain until
D. Safety Cases
code generation. Rhapsody has a precisely defined semantics
To argue about the safety of systems, Safety Cases are [29]. It has even been used as a basis to provide integrated
a proven technique that allows a systematic argumentation. formal verification [30]. However, it is not as tightly integrated
Safety Cases may contain complex arguments that can be as AUTO FOCUS 3, not open source and is essentially used for
decomposed corresponding to modular system artifacts which commercial use and not as a platform for research experiments
are generally dependent on artifacts from different viewpoints: as AUTO FOCUS 3. The design space exploration viewpoint
e.g., requiring redundancy for safety has an impact both on of AUTO FOCUS 3 is a research tooling concept which is
software and on hardware architectures. Such assurance cases a good example of such an experiment which differenti-
ates AUTO FOCUS 3 from Rhapsody. Similar considerations
hold for Bridgepoint (or xtUML)4 , LieberLieber Embedded
Engineer5 and the Enterprise Architect (EA)6 that supports
many modeling languages such as UML or SysML. ADORA
(Analysis and Description of Requirements and Architecture)7
is a research tool that supports an object-oriented method
and a modeling language also called ADORA [31]. ADORA
targets requirements and the software architecture of a system.
Hardware is not included.
Ptolemy II [32] is similar to AUTO FOCUS 3 in the sense
Fig. 26. GSN-based Safety Cases that it is based on formal semantics and provides code genera-
tion. Like AUTO FOCUS 3, it is an open source and academic
are generally not well integrated with the different system tool which is used for research. However, Ptolemy targets
models, resp. viewpoints. To provide a comprehensible and only the software architecture: neither requirements nor the
reproducible argumentation and evidence for argument cor- hardware are integrated. This arises from the fact that the
rectness, we make use of the integrated system model. Since 1 https://wiki.eclipse.org/Papyrus/UserGuide/ModelExecution
AUTO FOCUS 3 provides such integrated models at its core, it 2 http://projects.eclipse.org/proposals/diversity
3 www-01.ibm.com/software/awdtools/rhapsody/
leverages the possibility to tightly connect these system models
4 https://xtuml.org/
with safety case artefacts in order to form a comprehensive 5 http://www.lieberlieber.com/en/embedded-engineer-for-enterprise-
safety argumentation. In AUTO FOCUS 3 we provide safety architect/
case modelling based on Goal Structuring Notation (GSN) 6 http://www.sparxsystems.com/products/ea/index.html
[25], as illustrated Fig. 26. Different safety case artifacts can be 7 http://www.ifi.uzh.ch/rerg/research/adora.html
development of embedded systems is not the main focus of [11] M. Feilkas, F. Hölzl, C. Pfaller, S. Rittmann, B. Schätz, W. Schwitzer,
Ptolemy. W. Sitou, M. Spichkova, and D. Trachtenherz, “A Refined Top-
Down Methodology for the Development of Automotive Software
The SCADE Suite8 is a commercial tool well-known in Systems: The KeylessEntry System Case Study,” Technische Universität
the development of control software, for example in avionics. München, Tech. Rep. TUM-I1103, Februar 2011.
While the SCADE Suite9 offers a lot of functionality with [12] W. Böhm, M. Junker, A. Vogelsang, S. Teufl, R. Pinger, and K. Rahn, “A
formal systems engineering approach in practice: an experience report,”
respect of simulation, verification and code generation, at the in 1st International Workshop on Software Engineering Research and
moment it does not provide any support for requirements. Industrial Practices, SER&IPs, Hyderabad, India, June 2014, pp. 34–41.
[13] B. Bernhard Schätz, “Model-based development of soft-
ware systems: From models to tools.” Habilitation Thesis,
V. C ONCLUSION Technische Universität München, 2009. [Online]. Available:
http://www4.in.tum.de/ schaetz/papers/Habiliationsschrift.pdf
In this paper, we presented AUTO FOCUS 3 and the tooling [14] P. Bishop and R. Bloomfield, “A methodology for safety case devel-
concepts that it supports at different steps in the development opment,” in Safety-Critical Systems Symposium. Birmingham, UK:
process. AUTO FOCUS 3 is based on a completely integrated Springer-Verlag, ISBN 3-540-76189-6, Feb 1998.
[15] M. Dwyer, G. Avrunin, and J. Corbett, “Patterns in property specifica-
model-based development approach from requirements elici- tions for finite-state verification,” in ICSE, 1999.
tation to deployment on the platform of code which allows to [16] R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli,
generate code completely (i.e., without further human modi- S. Mover, M. Roveri, and S. Tonetta, “The nuxmv symbolic model
checker,” in Computer Aided Verification. Springer International
fication) from the models. Based on well-defined semantics, Publishing, 2014, pp. 334–342.
AUTO FOCUS 3 demonstrates how integrated models are [17] F. Consortium, “Flexray communications system protocol specification,
enablers for a wide range of analysis and synthesis tech- version 2.1, revision A,” URL http://www.flexray.com, 2005.
[18] D. Mou and D. Ratiu, “Binding requirements and component architec-
niques such as testing, model checking and deployment and ture by using model-based test-driven development,” in Twin Peaks of
scheduling synthesis. Tooling concepts in AUTO FOCUS 3 Requirements and Architecture (Twin Peaks), 2012.
demonstrate how to make use of these techniques in a model- [19] J. O. Blech, D. Mou, and D. Ratiu, “Reusing test-cases on different levels
of abstraction in a model based development tool,” in MBT, 2012, pp.
based development process. 13–27.
[20] S. Li, S. Balaguer, A. David, K. Larsen, B. Nielsen, and S. Pusinskas,
R EFERENCES “Scenario-based verification of real-time systems using uppaal,” Formal
Methods in System Design, vol. 37, no. 2-3, pp. 200–264, 2010.
[1] M. Broy and K. Stølen, Specification and Development of Interactive [21] S. Voss and B. Schätz, “Scheduling shared memory multicore architec-
Systems: Focus on Streams, Interfaces, and Refinement. Springer, 2001. tures in AF3 using Satisfiability Modulo Theories,” in MBEES, 2012,
[2] K. Pohl, H. Hönninger, R. Achatz, and M. Broy, Model-Based Engi- pp. 49–56.
neering of Embedded Systems: The SPES 2020 Methodology. Springer [22] L. De Moura and N. Bjørner, “Z3: An efficient SMT solver,” Tools and
Publishing Company, Incorporated, 2012. Algorithms for the Construction and Analysis of Systems, pp. 337–340,
2008.
[3] U.S. Office of Management and Budget and U.S. Office of E-
[23] S. Voss, J. Eder, and F. Hölzl, “Design space exploration and
Government and IT, “A Common Approach to Federal Enterprise
its visualization in AUTOFOCUS3,” in Gemeinsamer Tagungsband
Architecture.”
der Workshops der Tagung Software Engineering, Kiel, Deutschland,
[4] F. Huber, B. Schätz, A. Schmidt, and K. Spies, “AutoFocus - A Tool for
25.-26. Februar 2014 2014, pp. 57–66. [Online]. Available: http://ceur-
Distributed Systems Specification,” in Formal Techniques in Real-Time
ws.org/Vol-1129/paper33.pdf
and Fault-Tolerant Systems (FTRTFT), ser. LNCS, vol. 1135. Springer
[24] F. Hölzl, “The AutoFocus 3 C0 Code Generator,” Technische Universität
Verlag, 1996, pp. 467–470.
München, Tech. Rep. TUM-I0918, 2009.
[5] F. Hölzl and M. Feilkas, “Autofocus 3: A scientific tool prototype
[25] T. Kelly and R. Weaver, “The goal structuring notation – a safety
for model-based development of component-based, reactive, distributed
argument notation,” in Proc. of Dependable Systems and Networks 2004
systems,” in Proceedings of the 2007 International Dagstuhl Conference
Workshop on Assurance Cases, 2004.
on Model-based Engineering of Embedded Real-time Systems, ser.
[26] S. Voss, C. Cârlan, B. Schätz, and T. Kelly, “Safety case driven model-
MBEERTS’07. Berlin, Heidelberg: Springer-Verlag, 2010, pp. 317–
based systems construction,” in EITEC, 2015.
322.
[27] S. Gérard, C. Dumoulin, P. Tessier, and B. Selic, “Papyrus: A UML2 tool
[6] S. Teufl, D. Mou, and D. Ratiu, “MIRA: A tooling-framework to for domain-specific language modeling,” in Model-Based Engineering
experiment with model-based requirements engineering,” in 21st IEEE of Embedded Real-Time Systems - International Dagstuhl Workshop,
International Requirements Engineering Conference, RE, Rio de Janeiro- Dagstuhl Castle, Germany, November 4-9 2007, pp. 361–368, revised
RJ, Brazil, 2013, pp. 330–331. Selected Papers.
[7] A. Campetelli, F. Hölzl, and P. Neubeck, “User-friendly model checking [28] T. O. M. Group, Semantics of a Foundational Subset for Executable
integration in model-based development,” in 24th International Confer- UML Models (FUML). Pearson Higher Education, 2013. [Online].
ence on Computer Applications in Industry and Engineering (CAINE), Available: http://www.omg.org/spec/FUML/1.1
November 2011. [29] D. Harel and H. Kugler, “The rhapsody semantics of statecharts (or, on
[8] S. Voss, J. Eder, and F. Hölzl, “Design space exploration and its the executable core of the uml),” in Integration of Software Specification
visualization in AUTOFOCUS3,” in Gemeinsamer Tagungsband der Techniques for Applications in Engineering, ser. Lecture Notes in
Workshops der Tagung Software Engineering, Kiel, Deutschland, 25.- Computer Science. Springer Berlin Heidelberg, 2004, vol. 3147, pp.
26. Februar 2014, pp. 57–66. 325–354.
[9] T. Kelly, C. Carlan, and S. Voss, “Model-based safety cases in autofo- [30] I. Schinz, T. Toben, C. Mrugalla, and B. Westphal, “The rhapsody uml
cus3,” in 1st International Workshop on Assurance Cases for Software- verification environment,” in Proceedings of the Software Engineering
intensive Systems (ASSURE), 2013, tool demonstration. and Formal Methods, Second International Conference, ser. SEFM.
[10] M. Feilkas, A. Fleischmann, F. Hölzl, C. Pfaller, K. Scheidemann, Washington, DC, USA: IEEE Computer Society, 2004, pp. 174–183.
M. Spichkova, and D. Trachtenherz, “A top-down methodology for the [31] M. Glinz, S. Berner, and S. Joos, “Object-oriented modeling with adora,”
development of automotive software,” Technische Universität München, Inf. Syst., vol. 27, no. 6, pp. 425–444, Sep. 2002.
Tech. Rep. TUM-I0902, January 2009. [32] J. Eker, J. W. Janneck, E. A. Lee, J. Liu, X. Liu, J. Ludvig, S. Neuen-
dorffer, S. R. Sachs, and Y. Xiong, “Taming heterogeneity - the ptolemy
8 http://www.esterel-technologies.com/products/scade-suite/ approach,” Proceedings of the IEEE, vol. 91, no. 1, pp. 127–144, 2003.
9 http://www.esterel-technologies.com/products/scade-suite/