Refinement and implementation techniques for Abstract State Machines [Elektronische Ressource] / Joachim Schmid

Joachim Schmid

Sujets

• Informatik

Informations

• Publié par: universitat_ulm
• Publié le: 01 janvier 2002
• Nombre de lectures: 16
• Langue: Deutsch

Extrait

Refinement and
Implementation Techniques
for
Abstract State Machines
Dissertation
zur Erlangung des Grades eines Doktors
der Naturwissenschaften (Dr. rer. nat.)
im Fachbereich Informatik
der Universit¨at Ulm
vorgelegt von
Joachim Schmid
aus Tuttlingen
Abteilung fur¨ Programmiermethodik und Compilerbau
(Leiter: Prof. Dr. Helmuth Partsch)
2002II
Amtierender Dekan: Prof. Dr. Gu¨nther Palm
Gutachter: Prof. Dr. Helmuth Partsch (Universit¨at Ulm)
Prof. Dr. Friedrich von Henke (Universit¨at Ulm)
Prof. Dr. Egon B¨orger (Universit¨at Pisa)
Tag der Pruf¨ ung: 17. Juni 2002Danksagung
An dieser Stelle m¨ochte ich mich bei allen Personen bedanken, die mich bei der
Erstellung dieser Arbeit unterstutzt¨ haben.
Besonderen Dank gilt Herrn Prof. Dr. Egon B¨orger, der stets ein offenes
Ohr fu¨r Fragen und Diskussionen hatte und mich zu dieser Arbeit motivierte.
Bedankenm¨ochteichmichfur¨ dietatkraftig¨ eUnterstut¨ zungdurchDr. Peter
P¨appinghaus, der meine Promotion bei der Siemens AG betreute. Dank gilt
auch allen anderen Mitarbeitern von CT SE 4, welche manchmal von ihrer
Arbeit abgehalten wurden.
Dank gilt der Siemens AG, die mir die notwendigen Arbeitsmittel zur Verfu-¨
gung stellte und mich finanziell unterstu¨zte. Insbesondere moc¨ hte ich mich bei
dem Fachzentrumsleiter Prof. Dr. Wolfram Bu¨ttner bedanken, der sich bereit
erkl¨art hatte, diese Dissertation durch die Siemens AG zu unterstutze¨ n.
IIIContents
Introduction 1
1 Submachine Concept 3
1.1 Standard ASMs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
1.2 Sequential Composition and Iteration . . . . . . . . . . . . . . . 5
1.2.1 Sequence Constructor . . . . . . . . . . . . . . . . . . . . 6
1.2.2 Iteration Constructor . . . . . . . . . . . . . . . . . . . . 8
1.2.3 B¨ohm-Jacopini ASMs . . . . . . . . . . . . . . . . . . . . 10
1.3 Parameterized Machines . . . . . . . . . . . . . . . . . . . . . . . 13
1.4 Further Concepts . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
1.4.1 Local State . . . . . . . . . . . . . . . . . . . . . . . . . . 15
1.4.2 ASMs with Return Value . . . . . . . . . . . . . . . . . . 16
1.4.3 Error Handling . . . . . . . . . . . . . . . . . . . . . . . . 17
1.5 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2 Component Concept 19
2.1 Component . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.1.1 Formal Definition . . . . . . . . . . . . . . . . . . . . . . . 20
2.1.2 Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . 23
2.1.3 Verification . . . . . . . . . . . . . . . . . . . . . . . . . . 23
2.1.4 Defining Components . . . . . . . . . . . . . . . . . . . . 25
2.2 Composition of Components . . . . . . . . . . . . . . . . . . . . . 31
2.2.1 Formal Definition . . . . . . . . . . . . . . . . . . . . . . . 31
2.2.2 Defining Composition . . . . . . . . . . . . . . . . . . . . 37
2.3 Component based Verification . . . . . . . . . . . . . . . . . . . . 41
2.4 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
3 Execution of Abstract State Machines 51
3.1 Functional Programming and ASMs . . . . . . . . . . . . . . . . 51
3.2 Lazy Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
3.3 Lazy Evaluation and ASMs . . . . . . . . . . . . . . . . . . . . . 54
3.3.1 Nullary Dynamic Functions . . . . . . . . . . . . . . . . . 54
3.3.2 Firing Rules . . . . . . . . . . . . . . . . . . . . . . . . . . 56
3.3.3 Unary Dynamic Functions . . . . . . . . . . . . . . . . . . 57
3.3.4 Referential Transparency . . . . . . . . . . . . . . . . . . 59
3.4 Sequential Execution of Rules . . . . . . . . . . . . . . . . . . . . 62
3.5 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
VVI CONTENTS
4 The AsmGofer System 65
4.1 The Interpreter . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
4.1.1 Expression Evaluation . . . . . . . . . . . . . . . . . . . . 66
4.1.2 Dealing with Files . . . . . . . . . . . . . . . . . . . . . . 66
4.1.3 Other Commands . . . . . . . . . . . . . . . . . . . . . . 67
4.2 Sequential ASMs . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
4.2.1 Nullary Dynamic Functions . . . . . . . . . . . . . . . . . 68
4.2.2 Unary Dynamic Functions . . . . . . . . . . . . . . . . . . 70
4.2.3 Update Operator . . . . . . . . . . . . . . . . . . . . . . . 71
4.2.4 N-ary Dynamic Functions . . . . . . . . . . . . . . . . . . 71
4.2.5 Execution of Rules . . . . . . . . . . . . . . . . . . . . . . 72
4.2.6 Rule Combinators . . . . . . . . . . . . . . . . . . . . . . 73
4.3 Distributed ASMs . . . . . . . . . . . . . . . . . . . . . . . . . . 74
4.4 An Example: Game of Life . . . . . . . . . . . . . . . . . . . . . 76
4.4.1 Static Semantics . . . . . . . . . . . . . . . . . . . . . . . 76
4.4.2 Dynamic Semantics . . . . . . . . . . . . . . . . . . . . . 78
4.5 Automatic GUI Generation . . . . . . . . . . . . . . . . . . . . . 79
4.6 User defined GUI . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
5 Applications 85
5.1 The Light Control System . . . . . . . . . . . . . . . . . . . . . . 85
5.2 Java and the Java Virtual Machine . . . . . . . . . . . . . . . . . 85
5.3 Hardware Verification . . . . . . . . . . . . . . . . . . . . . . . . 86
5.4 FALKO . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
Conclusions and Outlook 89
Zusammenfassung 93
Appendix 95
A Submachine Concept 95
A.1 Deduction Rules for Update Sets . . . . . . . . . . . . . . . . . . 95
B Component Concept 99
B.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
B.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100
B.3 Type system . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102
B.4 Constraints . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104
References 105Introduction
ThenotionofAbstractStateMachines(ASMs), definedbyGurevichin[33,34],
has been used successfully for the design and the analysis of numerous complex
software and hardware systems (see [16] for an overview). The outstanding
features which are responsible for this success are the simple yet most general
notion of state—namely mathematical structures, providing arbitrary abstract
datatypes—togetherwiththesimultaneousexecutionofmultipleatomicactions
as the notion of state transforming basic machine step.
Thisview,ofmultipleatomicactionsexecutedinparallelinacommonstate,
comes however at a price: the standard composition and structuring principles,
which are needed for high-level system design and programming in the large,
are not directly supported and can be introduced only as refinement steps. Also
the freedom in the choice of the appropriate data structures, which provides a
powerful mechanism to describe systems at various levels of abstraction, has a
price: it implies an additional step to turn these abstractions into executable
models, so that experimental validation can be done via simulation.
In this thesis we enhance the usefulness of ASMs for software engineering
practice by:
• defining three major composition concepts for ASMs, namely component
machine, parameterized submachine, and iteration, which cannot be dis-
pensed with in software engineering (Chap. 1, Chap. 2)
• developing a tool that allows to execute these extended ASMs and comes
withagraphicaluserinterface, tosupportexperimentalanalysis(Chap.3,
Chap. 4)
We havetestedthepracticalityoftheproposedconcepts andoftheirimplemen-
tation (Chap. 5), namely by the design and the analysis
• of a well-known software engineering case study in the literature and of a
middlesizedindustrialsoftwaredevelopmentproject(foratraintimetable
construction and validation system). This project work also included the
development of a proprietary compiler from ASMs to C++.
• of the Java language and its implementation on the Java Virtual Machine
• of an industrial ASIC design and verification project. This project work
also included the development of a compiler from ASM components to
VHDL.
Part of this work has been published already in [17, 18, 19, 61, 63, 64].
12 Introduction
Notational conventions
Throughout this thesis we stick to standard mathematical terminology. Never-
theless, we list here some frequently used notations.
We writeP(X) for the set of all subsets of X.
We write Xf for the domain restriction of the function f to the set X:
Xf :={(x,f(x))| x∈ dom(f)∩X}
We use ε for the empty sequence and· to separate elements in a sequence.
≥nFurther,wewriteR fortheuniversecontainingallsequencesofR withlength
greater or equal than n.
≥n n n+1R = R ∪R ∪ ...
nR = R·...·R
| {z }
n
Sinceonlysomefunctionsarepartialinthisthesiswedenotethembythesymbol
→ instead of symbol→ for total functions. For example:
f : R → R1 2
The composition of functions is denoted by f◦g.
We useN to denote the set of natural numbers from zero to n.n
77Chapter 1
Submachine Concept
It has often been observed that Gurevich’s definition of Abstract State Ma-
chines (ASMs) [33] uses only conditional assignments and supports none of the
classical control or data structures. On the on