SENG405 Formal Methods in Software Engineering

SENG405 Reading List

Thompson, Heimdahl, Miller, 1999, "Specification-based prototyping for Embedded Systems", Proceedings of the 7th European engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering

Kumar, Li, 2002, "Using Model Checking to Debug Device Firmware", Proceedings of 5th USENIX Symposium on Operating Systems Design and Implementation (OSDI’2002).

Cleaveland, 1999, "Pragmatics of Model Checking:an STTT special section", Software Tools for Technology Transfer 2(3): 208-218, November 1999. (C)1999 Springer-Verlag

Alon, Milo, Neven, Suciu, Vianu, 2003, "Typechecking XML Views of Relational Databases", ACM Transactions on Computational Logic (TOCL)

Burdy, Cheon, Cok,, Earnst, Kiniry, Leavens, Leino, Poll, 2002, "An overview of JML tools and applications", Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 03), (Trondheim, Norway), June 5-7, 2003

Butler, 1996, "An introduction to Requirements Capture using PVS: Specification of a Simple Autopilot", NASA TM-110255, May 1996

McMillan, 2000, "The SMV system"

"Entity Management" - OASIS Technical Resolution 9401:1997 (Amendment 2 to TR 9401)

Rustin, Leino, Nelson, Saxe, 2000, "ESC/Java User's Manual"

Councill, Heineman, "Component-Based Software Engineering: Definition of a Software Component and Its Elements",

David M Weiss, "Information Hiding"

Parnas, "On the Criteria to be used in decomposing Systems into Modules",

"Formal Methods Specification and Verification Guidebook for Software and Computer Systems: Volume 1 Planning and Technology Insertion" (1998)

CCITT Specification and Description Language (SDL), 1992

Odegard - "Edison: Towards a formal methods based programming environment and language for robust distributed systems.", 1998

SENG405 Reading List - Example Specification

W3C, 2000, "Extensible Markup Language (XML) 1.0 (Second Edition)"

SENG405 Reading List - Haskell

Simon Peyton Jones, ????, "Haskell 98 Language and Libraries"

SENG405 Reading List - Erlang

Armstrong, Virding, Wikstrom, Williams, "Concurrent Programming in Erlang", Prentice-Hall

Joe Armstrong, "Getting Erlang to talk to the outside world",

WWW

Ken McMillan - Lecture notes for NATO summer school on verification of digital and hybrid systems - http://www-cad.eecs.berkeley.edu/~kenmcmil/tutorial/toc.html

Discussion

Everything connects.
- Risk
- Methods
- Languages
- Simplicity

Methods

It is not the modelling tools, systems or programming languages as such that defines the task, but what you want to do and how you can do it easily. Formal methods introduces formal notations upfront in order to minimise the risk of the development. Take the example of string manipulation: in which apparantly simple specifications can get caught out. We need to reduce risk, and one of those ways of doing that is to describe our problem in a simple language which we can easily check. This is where formal methods comes in and is the reason for a potential productivity improvment.

Risk

Risk is avoided through formalising models, using languages such as CTL - Computational Tree Logic - which is useful for discovering problems to do with race conditions and parallelism with interdependency.

Simplicity

Formal Models provide a level of simplicity: easy to read, easy to understand, easy to use. This enables critical model checking to take place early on in the software development process, reducing the cost of errors down the line.

Languages for Formal Specification

The languages for making these basic descriptions vary from mathematical ones to logic based languages like CTL. Different languages provide a different view of our models. Specification languages can be used to specify the way in which we want to implement our requirements. Specification languages can be built using mathematically checkable formulas, enabling correctness of the models to be proved. Another approach to formalism is to tightly define our component structures, and insert checkers in between the communicating parties - this can take the form of contract checkers, as in the Armstrong Paper "Getting Erlang to talk to the outside world".