287 Pages
English

Specification and seamless verification of embedded real-time systems [Elektronische Ressource] : FOCUS on Isabelle / Maria Spichkova

Gain access to the library to view online
Learn more

Informations

Published by
Published 01 January 2007
Reads 16
Language English
Document size 1 MB

Specification and Seamless Verification of
Embedded Real-Time Systems:
FOCUS on Isabelle
Maria Spichkova
Lehrstuhl fur¨ Software&Systems Engineering
Institut fu¨r Informatik
Technische Universit¨at Munchen¨Lehrstuhl fur¨ Software & Systems Engineering
Institut fur¨ Informatik
Technische Universit¨at Munch¨ en
Specification and seamless verification of embedded
real-time systems:
FOCUS on Isabelle
Maria Spichkova
Vollst¨andiger Abdruck der von der Fakult¨at fu¨r Informatik der Technischen
Universit¨at Munc¨ hen zur Erlangung des akademischen Grades eines
Doktors der Naturwissenschaften (Dr. rer. nat.)
genehmigten Dissertation.
Vorsitzender: Univ.-Prof. Dr. Helmut Seidl
Pruf¨ er der Dissertation:
1. Univ.-Prof. Dr. Dr. h.c. Manfred Broy
2. Univ.-Prof. Tobias Nipkow, Ph.D.
DieDissertationwurdeam13.06.2007beiderTechnischenUniversit¨atMu¨nchen
eingereicht und durch die Fakult¨at fu¨r Informatik am 28.09.2007 angenommen.Abstract
The purpose of this thesis is to create a coupling of the formal specification
frameworkFocus in the generic theorem prover Isabelle/HOL, a logical frame-
work based on Higher-Order Logic. The main focus of this work is on specifi-
cation and verification of systems that are especially safety critical – embedded
real-time systems.
Isabelle/HOL is an interactive semi-automatic theorem prover and in the
proofs of some system properties human time must be invested. These proofs
strongly depend on the specifications of the system and the properties. By con-
sidering the framework “Focus on Isabelle”, which is result of the coupling, we
can influence the complexity of proofs already during the specification phase,
e.g. reformulating specification to simplify the Isabelle/HOL proofs for a trans-
lated Focus specification. Thus, the specification and verification/validation
methodologies are treated as a single, joined, methodology with the main fo-
cus on the specification part. This methodology uses particularly the idea of
refinement-basedverification,wheretheverificationofsystempropertiescanbe
treatedasavalidationofasystemspecificationwithrespecttothespecification
representing the properties.
The key contributions of the thesis are
X Deep embedding of that part of the framework Focus, which is ap-
propriate for the specification of real-time systems, into Isabelle/HOL.
“Focus on Isabelle” enables to validate and verify system specifications
in a methodological way.
X Syntax extensions for Focus for the argumentation over time intervals:
a special kind of tables, timed state transition diagrams, and a number of
new operators. The deep embedding into Isabelle/HOL includes all these
extensions.
X Schemata forautomatic correctness proofs in Isabelle/HOL of the syntac-
tic interfaces for specified system components.
The feasibility of the proposed approach was evaluated on three case studies
that cover different application areas:
X Steam Boiler System (process control),
X FlexRay communication protocol (data transmission),
X Automotive-Gateway System (memory and processing components, data
transmission).
The results of “Focus on Isabelle” can also be extended to a complementary
approach, “Janus on Isabelle”, that presents a coupling of the formal specifi-
cation framework for services, Janus, with Isabelle/HOL.
iiiAcknowledgements
I would like to thank all those people that have helped me, either directly
or indirectly, with the development of this thesis.
My special thanks go to my supervisor Manfred Broy. He gave me the op-
portunity to work in a highly qualifed research group and guided my activity
in the past four years. His own work provided much of the motivation of this
thesis. Furthermore, I want to thank Manfred Broy for all his well-founded and
helpful advice and support, as well as for directing me towards the concrete
topic of my thesis.
Special thanks go also to Tobias Nipkow for being my referee and improving
the quality of the realization with his technical advice.
Thanks are due to all my colleagues for years of discussion. In particular I
am grateful to thank my colleagues Stefan Berghofer and Clemens Ballarin for
carefully reading draft version of this thesis and suggesting numerous improve-
ments. I also would like to thank Oscar Slotosch, Bernhard Rumpe, Alexander
Ziegler, Bernhard Sch¨atz, Daniel Ratiu, Christian Ku¨hnel, Martin Wildmoser,
and Borislav Gajanovic for inspiring and clarifying discussions.
Last but not least, I want to thank my mother for her continuous support
and encouragement during the work.
iiiivContents
1. Introduction 1
1.1. Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2. Isabelle/HOL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.3. FOCUS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.3.1. Concept of Streams . . . . . . . . . . . . . . . . . . . . . 6
1.3.2. Operators on Streams . . . . . . . . . . . . . . . . . . . . 7
1.3.3. Specification Styles . . . . . . . . . . . . . . . . . . . . . . 10
1.3.4. Elementary and Composite Specifications . . . . . . . . . 10
1.3.5. Sheaves and Replications . . . . . . . . . . . . . . . . . . 13
1.3.6. Refinement . . . . . . . . . . . . . . . . . . . . . . . . . . 14
1.3.7. Causality . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
1.4. JANUS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
1.5. Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2. Focus on Isabelle 21
2.1. Specification of Embedded Real-Time Systems . . . . . . . . . . 22
2.2. Stream Representation . . . . . . . . . . . . . . . . . . . . . . . . 23
2.3. Representation of Datatypes . . . . . . . . . . . . . . . . . . . . . 26
2.4. FOCUS Operators Representation . . . . . . . . . . . . . . . . . 28
2.4.1. nth Message of a Stream . . . . . . . . . . . . . . . . . . . 28
2.4.2. Length of a Stream . . . . . . . . . . . . . . . . . . . . . . 29
2.4.3. Concatenation Operator . . . . . . . . . . . . . . . . . . . 29
2.4.4. Prefix of a Stream . . . . . . . . . . . . . . . . . . . . . . 30
2.4.5. Truncate a Stream . . . . . . . . . . . . . . . . . . . . . . 31
2.4.6. Domain and Range of a Stream . . . . . . . . . . . . . . . 32
2.4.7. Time-synchronous Stream . . . . . . . . . . . . . . . . . . 33
2.4.8. Make Untimed . . . . . . . . . . . . . . . . . . . . . . . . 34
2.4.9. Time Stamp Operator . . . . . . . . . . . . . . . . . . . . 34
2.4.10. Filtering Operator . . . . . . . . . . . . . . . . . . . . . . 35
2.4.11. Application Operator . . . . . . . . . . . . . . . . . . . . 36
2.4.12. Stuttering Removal Operator . . . . . . . . . . . . . . . . 36
2.5. FOCUS Operators: Extensions . . . . . . . . . . . . . . . . . . . 37
2.5.1. Number of Time Intervals in a Finite Stream . . . . . . . 37
2.5.2. Timed Truncation Operator . . . . . . . . . . . . . . . . . 37
2.5.3. Time Interval . . . . . . . . . . . . . . . . . . . . . . . . . 38
2.5.4. Drop a Stream . . . . . . . . . . . . . . . . . . . . . . . . 39
2.5.5. Timed Merge . . . . . . . . . . . . . . . . . . . . . . . . . 40
vContents
2.5.6. Concatenation of Time Intervals . . . . . . . . . . . . . . 41
2.5.7. Limited Number of Messages . . . . . . . . . . . . . . . . 42
2.5.8. Stuttering Removal Operator for Timed Streams . . . . . 44
2.5.9. Changing Time Granularity . . . . . . . . . . . . . . . . . 44
2.5.10. Deleting the First Time Interval . . . . . . . . . . . . . . 46
2.5.11. First Nonempty Time Interval . . . . . . . . . . . . . . . 46
2.5.12. Index of the First Nonempty Time Interval . . . . . . . . 48
2.5.13. Last Nonempty Time Interval . . . . . . . . . . . . . . . . 49
2.6. tiTable . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
2.7. Encapsulated States . . . . . . . . . . . . . . . . . . . . . . . . . 54
2.8. Timed State Transition Diagrams . . . . . . . . . . . . . . . . . . 56
2.9. Mutually Recursive Functions . . . . . . . . . . . . . . . . . . . . 59
2.10.Time-Synchronous Streams . . . . . . . . . . . . . . . . . . . . . 59
2.11.Isabelle/HOL Semantics of Elementary and Composite FOCUS
Specifications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
2.11.1. Auxiliary Datatypes, Functions and Predicates . . . . . . 61
2.11.2. Elementary Specification. . . . . . . . . . . . . . . . . . . 62
2.11.3. Composite Specification . . . . . . . . . . . . . . . . . . . 65
2.11.4. Relations between Sets of Channels. . . . . . . . . . . . . 67
2.11.5. Example: Steam Boiler . . . . . . . . . . . . . . . . . . . 69
2.12.Composition types . . . . . . . . . . . . . . . . . . . . . . . . . . 73
2.12.1. Sequential composition. . . . . . . . . . . . . . . . . . . . 73
2.12.2. Parallel composition . . . . . . . . . . . . . . . . . . . . . 74
2.12.3. “Mix”-composition . . . . . . . . . . . . . . . . . . . . . . 75
2.12.4. Loop . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
2.13.Sheaves and Replications . . . . . . . . . . . . . . . . . . . . . . 79
2.13.1. Sheaves of Channels . . . . . . . . . . . . . . . . . . . . . 79
2.13.2. Specification Replications . . . . . . . . . . . . . . . . . . 82
2.13.3. Isabelle/HOL Specification of Relations between Sets of
Channels . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
2.13.4. Disjoint Channels in a Sheaf . . . . . . . . . . . . . . . . 90
2.13.5. Example: System with Sheaves of Channels . . . . . . . . 91
2.14.Translation schema: From FOCUS to Isabelle/HOL . . . . . . . 95
2.15.Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
3. Specification and Verification Methodology 105
3.1. Refinement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
3.1.1. Refinement Layers of a Specification Group . . . . . . . . 106
3.1.2. Behavioral Refinement . . . . . . . . . . . . . . . . . . . . 106
3.1.3. Interface Refinement . . . . . . . . . . . . . . . . . . . . . 109
3.1.4. Conditional Refinement . . . . . . . . . . . . . . . . . . . 109
3.2. Consistency of a Specification . . . . . . . . . . . . . . . . . . . . 110
3.3. Refinement-Based Verification . . . . . . . . . . . . . . . . . . . . 111
3.4. Key Ideas of the Specification and Verification Methodology . . . 114
3.5. Specification Hints and Mistakes . . . . . . . . . . . . . . . . . . 118
3.6. Complementary Approach: Janus on Isabelle . . . . . . . . . . . 120
vi