This book provides a comprehensive overview of automatic model refinement, which helps readers close the gap between initial textual specification and its desired implementation. The authors enable readers to follow two “directions” for refinement: Vertical refinement, for adding detail and precision to single description for a given model and Horizontal refinement, which considers several views on one level of abstraction, refining the system specification by dedicated descriptions for structure or behavior. The discussion includes several methods which support designers of electronic systems in this refinement process, including verification methods to check automatically whether a refinement has been conducted as intended.
|
|
|
1 | (6) |
|
|
|
5 | (2) |
|
|
|
7 | (16) |
|
|
|
7 | (6) |
|
2.1.1 The Unified Modeling Language UML |
|
|
8 | (3) |
|
2.1.2 The Object Constraint Language OCL |
|
|
11 | (2) |
|
2.2 Methodology: Model Finding |
|
|
13 | |
|
2.2.1 Model Finding in General |
|
|
13 | (3) |
|
2.2.2 Structural Model Finding |
|
|
16 | (1) |
|
2.2.3 Behavioral Model Finding |
|
|
17 | (2) |
|
|
|
19 | (4) |
|
3 Challenges in Model Refinement |
|
|
23 | (8) |
|
3.1 Example: A Phone Application |
|
|
24 | (1) |
|
3.2 Consistency in Vertical Refinement |
|
|
25 | (3) |
|
3.3 Consistency in Horizontal Refinement |
|
|
28 | (3) |
|
|
|
29 | (2) |
|
4 Verification of Vertical Refinement |
|
|
31 | (28) |
|
|
|
32 | (4) |
|
4.1.1 Rule-Based Model Refinement |
|
|
32 | (4) |
|
4.1.2 Formalization of the Refinement Relation |
|
|
36 | (1) |
|
4.2 Correctness of Refinement Relations |
|
|
36 | (11) |
|
|
|
37 | (1) |
|
4.2.2 Theoretical Foundation: Kripke Structures |
|
|
37 | (3) |
|
4.2.3 Verification Objectives |
|
|
40 | (2) |
|
4.2.4 Symbolic Representation of the Model and the Verification Objectives |
|
|
42 | (3) |
|
|
|
45 | (2) |
|
4.3 Slicing for Model Refinement |
|
|
47 | (9) |
|
|
|
49 | (1) |
|
4.3.2 Determining Relevant Model Elements |
|
|
50 | (4) |
|
|
|
54 | (2) |
|
|
|
56 | (3) |
|
|
|
57 | (2) |
|
5 Extraction of a Relation for Vertical Refinement |
|
|
59 | (20) |
|
|
|
60 | (1) |
|
5.2 Exact Relation Extraction |
|
|
61 | (9) |
|
5.2.1 Extraction with Subsequent Verification |
|
|
62 | (2) |
|
5.2.2 Extraction of a Correct Relation |
|
|
64 | (2) |
|
5.2.3 Discussion: Multiple Correct Relations |
|
|
66 | (2) |
|
|
|
68 | (2) |
|
5.3 Scenario-Based Relation Extraction |
|
|
70 | (4) |
|
5.3.1 Extraction of a Partial Relation |
|
|
70 | (2) |
|
|
|
72 | (2) |
|
5.4 Comparison of the Proposed Extraction Algorithms |
|
|
74 | (3) |
|
5.4.1 Exact Relation Extraction |
|
|
75 | (1) |
|
5.4.2 Scenario-Based Relation Extraction |
|
|
76 | (1) |
|
|
|
77 | (2) |
|
|
|
78 | (1) |
|
6 Verification of Horizontal Refinement |
|
|
79 | (14) |
|
|
|
80 | (1) |
|
6.2 Transformation from Activity Diagrams to OCL Constraints |
|
|
80 | (8) |
|
6.2.1 Assumptions About the Activity Diagram |
|
|
81 | (1) |
|
6.2.2 Normalization of the Activity Diagram |
|
|
82 | (4) |
|
6.2.3 Translation of the Normalized Diagram to OCL |
|
|
86 | (2) |
|
6.3 Verifying the Consistency Between Class and Activity Diagrams |
|
|
88 | (1) |
|
|
|
89 | (2) |
|
|
|
91 | (2) |
|
|
|
92 | (1) |
|
7 Summary and Conclusions |
|
|
93 | |
Julia Seiter currently works as a software architect at VEMAG Maschinenbau GmbH in Verden, Germany. She received the Diploma degree in computer science from the University of Bremen, Germany, in 2012. In 2015, she received her Dr.-Ing. degree, also from the University of Bremen, after having been with the Group of Computer Architecture for three years. Her research was focused on the design and verification of formal system models.
Robert Wille is a Full Professor at the Johannes Kepler University Linz. He received the Diploma and Dr.-Ing. degrees in computer science from the University of Bremen, Germany, in 2006 and 2009, respectively. He was with the Group of Computer Architecture at the University of Bremen and with the German Research Center for Artificial Intelligence (DFKI). Additionally, he worked as Lecturer at the University of Applied Science in Bremen, Germany, and as visiting professor at the University of Potsdam, Germany, and the Technical University Dresden, Germany. His research interests are in the design of circuits and systems for both conventional and emerging technologies with a focus in the domain of synthesis and verification.
Rolf Drechsler is head of Cyber-Physical Systems department at the German Research Center for Artificial Intelligence (DFKI) since 2011. Furthermore, he is a Full Professor at the Institute of Computer Science, University of Bremen, since 2001. Before, he worked for the Corporate Technology Department of Siemens AG, and was with the Institute of Computer Science, Albert-Ludwig University of Freiburg/Breisgau, Germany. Rolf Drechsler received the Diploma and Dr. Phil. Nat. degrees in computer science from the Goethe-University in Frankfurt/Main, Germany, in 1992 and, respectively, 1995. Rolf Drechsler focusses in his research at DFKI and in the Group for Computer Architecture, which he is heading at the Institute of Computer Science of the University of Bremen, on the development and design of data structures and algorithms with an emphasis on circuit and system design.
