Transcript Course Summary

Course Summary
Topics (1)
• Families of specification methods, evaluation
criteria
• Safety and liveness
• Expressing properties in predicate calculus
(logic)
• Input/output assertions, partial correctness,
Hoare logic, invariants
• Z notations: dom ran and special symbols
• Z schemas: defining the state, operations
• Z examples: symb. table, Unix files, telephone,...
Formal Specifications of Complex Systems
© Katz, 2007
-- Real-time 2
Topics (2)
• Schema calculus: modularity, hiding,...
• Refinement in Z: applying mapping functions,
data and operation refinement, applicability
and correctness
• State machine: pure graph, traces, using Z for
state machines
• Statecharts: superstates, parallelism, joint
transitions, history, micro-steps, activities
• Temporal logics, linear: [], <>,..., next
• Anchored version, past operators, classes of
properties, fairness
Formal Specifications of Complex Systems
© Katz, 2007
-- Real-time 3
Topics (3)
• Branching time: E, A, F, G, X, CTL
• Real time: TIME, Zeno, ranges, bound vars.
with temp. logic; for statecharts
• Lamport’s textual state machines: open versus
closed system, critical moment
• Allowed changes, parameter passing
• Fault tolerance, lossy queue and fairness,
alternating bit protocol impl. of queue
• Process algebras and LOTOS
• Nondeterminism, gates, actions,
• Process declaration and instantiation
Formal Specifications of Complex Systems
© Katz, 2007
-- Real-time 4
Topics (4)
•
•
•
•
Parallel comp.: |||, |[ gates ]|, | |, hiding
Offering (!) and accepting (?), negotiation
Stop, hiding, i, and multiway gates
Semantic views: bisimulation equivalence,
testing equiv., trace equiv.
• Algebraic specification and Larch, algebraic
axioms, initial/final algebra
• Generated by, partitioned by, converts
• Shared versus Interface Languages
Formal Specifications of Complex Systems
© Katz, 2007
-- Real-time 5
Three kinds of specifications
• Data and transition modeling:
Z vrs. Larch shared lang.;
For individual steps; textual, sequential
• Control:
Statecharts vrs. LOTOS (vrs. Esterelle vrs...)
For concurrency, overlap, synchronization
• Global liveness (and safety too):
Temporal logic in some version
Formal Specifications of Complex Systems
© Katz, 2007
-- Real-time 6
Present Use of Formal Specifications
• Invariants and I/O assertions: added to UML
designs, appear as run-time checks, assert
statements and checkers (in recent systems,
around 10% of Microsoft code)
• Elements of Z are in OCL (Object Constraint
Language) extension of UML
• Software model checkers
Bandera, accepts Java programs annotated with a
version of temporal logic
SLAM, a Microsoft product for checking temporal
logic assertions about driver software; now SDV
Java Pathfinder: NASA tool for model checking Java
Formal Specifications of Complex Systems
© Katz, 2007
-- Real-time 7
Present use (cont.)
• Feasibility checks for Java applets
No memory segment violations, no illegal operations >
• Legal requirements for formal specification and
verification using a tool, in addition to testing
Aircraft control >
Railway control in Europe and the US >
Software controlling nuclear reactors in Europe >
• Description languages for test data generation
• Hardware (design) verification using model
checking and/or simulation: widely used in
Intel, IBM, Motorola
Formal Specifications of Complex Systems
© Katz, 2007
-- Real-time 8
Trends
• Use formal methods selectively for problem areas
• Develop tools with clear added value
• Use for error detection as well as showing
correctness
• Set up environment where methods can be
combined (not yet widespread):
VeriTech: project to translate among verification tools >
and their specification notations
AOSD Formal Methods Lab: apply specification notations >
and verification tools to Aspect-Oriented Programming
Formal Specifications of Complex Systems
© Katz, 2007
-- Real-time 9
Realistically....
• Potential benefits are known.
• Problems with formal methods have become
evident.
• Modeling and tools have helped on real projects
in particular application areas.
• Software development is in so much trouble,
there is new willingness to invest in formal
methods.
Formal Specifications of Complex Systems
© Katz, 2007
-- Real-time 10