Unifying Theories of Programming and Formal Engineering Methods 1st Edition by Zhiminh Liu, Jim Woodcock, Huibiao Zhu ISBN 9783642397219 3642397212

1 Introduction

1.1 Software Complexity

1.2 Model-Driven Development

1.3 Formal Methods in Software Development

1.4 The Aim and Theme of rCOS

1.5 Organization

2 Unified Semantics of Sequential Programming

2.1 Designs of Sequential Programs

2.2 Designs of Object-Oriented Programs

2.3 Reactive Systems and Reactive Designs

3 Model of Primitive Closed Components

3.1 Specification Notation for Primitive Closed Components

3.2 Labeled Transition Systems of Primitive Closed Components

3.3 Component Contracts and Publications

3.4 Refinement between Closed Components

3.5 Separation of Concerns

4 Primitive Open Components

4.1 Specification of Open Components

4.2 Semantics and Refinement of Open Components

4.3 Transition Systems and Publications of Open Components

5 Processes

5.1 Specification of Processes

5.2 Contracts of Processes

5.3 Transition Systems and Publications of Processes

6 Architectural Compositions and General Components

6.1 Coordination of Components by Processes

6.2 Composition of Processes

6.3 Parallel Composition of Components

6.4 Renaming and Restriction

6.5 More Examples

7 Interface Model of Components

7.1 Component Automata

7.2 Non-blockable Provided Events and Traces

7.3 Interface Publication Automata

7.4 Composition and Refinement

8 Conclusions

References

Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems

1 Introduction

2 Timed Automata

2.1 Syntax and Semantics

2.2 Reachability

2.3 Regions

2.4 Behavioural Refinement Relations

2.5 Language Inclusion and Equivalence

2.6 Zones and Difference-Bound Matrices

3 Weighted Timed Automata

3.1 Optimal Reachability

3.2 Multi-weighted Timed Automata

3.3 Optimal Infinite Runs

3.4 Energy Problems

4 TimedGames

5 Statistical Model Checking for Networks of Price Timed Automata

5.1 Networks of Stochastic Automata

5.2 Verifying Queries Using Statistical Model Checking

5.3 Uppaal-SMC

5.4 Some Illustrations

References

Unifying Theories of Programming in Isabelle

1 Preliminaries

2 Introduction to UTP

3 Theory Mechanisation

4 The Alphabetised Relational Calculus

5 Laws of Programming

5.1 Conditional

5.2 Sequential Composition

5.3 Assignment

5.4 Nondeterminism

5.5 Alphabet Extension

5.6 Variable Blocks

6 The Complete Lattice

6.1 Lattice Operators

6.2 Recursion

6.3 Iteration

7 Hoare Logic

8 Weakest Preconditions

9 Designs

9.1 Lattice Operators

9.2 Refinement of Designs

9.3 Nontermination

9.4 Assignment

9.5 Closure under the Program Combinators

10 Healthiness Conditions

10.1 H1: Unpredictability

10.2 H2: Possible Termination

10.3 H3: Dischargeable Assumptions

10.4 H4: Feasibility

11 Related Work

12 Conclusion

References

FORMULA 2.0: A Language for Formal Specifications

1 DataandTypes

1.1 Constants

1.2 Data Constructors

1.3 Ordering of Values

1.4 Data Types and Subtyping

1.5 Type Declarations

1.6 Declaring Constants

1.7 Declaring Data Constructors

2 Domains and Models

2.1 Querying Models

2.2 Model Conformance

2.3 Relational Constraints

2.4 Finite Functions

2.5 Recursive Types, Aliases, and Symbolic Constants

2.6 Symbolic Constants

2.7 Separate Compilation

3 Rules and Domain Constraints

3.1 Derived Constants

3.2 Rule Bodies

3.3 Interpreted Functions

3.4 Type Environments

3.5 Set Comprehensions

3.6 General Rules and Rule Heads

3.7 Stratification and Termination

3.8 Complex Conformance Constraints

3.9 Extracting Proofs

4 Domain and Model Composition

4.1 Namespaces

4.2 Domain Composition

4.3 The Renaming Operator

5 Interpreted Functions

5.1 Arithmetic Functions and Identities

5.2 Boolean Functions

5.3 String Functions

5.4 List Functions

5.5 Coercion Functions

5.6 Reflection Functions

Formal Modelling, Analysis and Verification of Hybrid Systems

1 Introduction

1.1 Synopsis

2 Preliminaries

2.1 Continuous Dynamical Systems

2.2 Hybrid Systems

2.3 Polynomials and Polynomial Ideals

2.4 First-Order Theory of Reals

3 Computing Invariants for Hybrid Systems

3.1 Continuous and Global Invariant

3.2 Predicting Continuous Evolution via Lie Derivatives

3.3 Computing Transverse Set

3.4 Computing SCI in Simple Case

3.5 Computing SCI in General Case

3.6 SGI Generation

4 Switching Controller Synthesis

4.1 Problem Description

4.2 A Synthesis Procedure Based on CI Generation

4.3 Heuristics for Predefining Templates

4.4 Synthesis of Optimal Controllers

4.5 Oil Pump: A Case Study

5 HybridCSP

5.1 Notations

5.2 Operational Semantics

6 Hybrid Hoare Logic

6.1 History Formulas

6.2 Hoare Assertion

6.3 Proof System of HHL

6.4 Soundness

7 HHL Prover

7.1 Expressions

7.2 Assertion Language

7.3 HCSP

7.4 Semantics

7.5 Proof System of HHL

8 Case Study: Chinese Train Control System

8.1 Movement Authority Scenario

8.2 Level Transition

8.3 Mode Transition

8.4 Combined Scenario and Its Model

8.5 Proof of the Combined Scenario

9 Other Issues: Stability Analysis

9.1 Lyapunov Stability

9.2 Relaxed Lyapunov Function

9.3 Automatically Discovering Polynomial RLFs for PCDSs

9.4 Simplification and Implementation

9.5 Example

10 Conclusion

References

Author Index

People also search for Unifying Theories of Programming and Formal Engineering Methods 1st Edition :