Reference Library Formal Methods
	This page provides access to a variety of downloadable papers that address formal methods issues. The following topics are considered: General Object Constraint Language (OCL) General An Introduction to Z and Formal Specifications [PDF] J.M. Spivey This paper describes information systems using formal, mathematical specifications written in the Z notation. These specifications are then refined into rigorously checked designs. This paper first introduces formal specification using and example, then introduces the idea of data refinement as a primary means for constructing designs which achieve a formal specification using examples. Formal Development Methods for Interactive Systems: Combining Interactors and Design Rationale [PDF] Christopher John Bramwell This thesis builds upon existing research on the formal aspects of human-computer interaction by providing practical specification and development methods for interactive systems. The specification style used is based on the abstract concept of interactors, which has been used extensively at York. The development methods are integrated with a way in which design options that occur may be recorded and choices between them made so that a more constructive development process is provided between the programmer and the client. Formalization of Software Testing Criteria using the Z Notation [PDF] Sergiy A. Vilkomir and Jonathan P. Bowen This paper describes an approach to formalization of criteria of computer systems software testing. A brief review of control-flow criteria is introduced. As a formal language for describing the criteria, the Z notation is selected. Z schemas are presented for definitions of the following criteria: statement coverage, decision coverage, condition coverage, decision/condition coverage, full predicate coverage, modified condition/decision coverage, and multiple condition coverage. This characterization could help in the correct understanding of different types of testing and also the correct application of a desired testing regime. Formal Methods in Practice: the Missing Link A Perspective from the Security Area [PDF] D. Bolignano, D. Le Métayer and C. Loiseaux This slide presentation presents the following topics: potential benefits of formal methods, evaluation assurance levels, building on existing documentation, establishing links between informal, semi-formal and formal methods, what to specify and how, an example: the Java Card VM, specifying and proving in the large, dealing with systems rather than components, using appropriate tools, explaining and justifying specs and proofs, integration of formal methods in a traditional development environment, illustration: test suite generation, and assess the benefits of the formalization. Formal Specification: A Roadmap [PDF] Axel van Lamsweerde Formal specifications have been a focus of software engineering research for many years and have been applied in a wide variety of settings. Their industrial use is still limited but has been steadily growing. After recalling the essence, role, usage, and pitfalls of formal specification, the paper reviews the main specification paradigms to date and discuss their evaluation criteria. It then provides a brief assessment of the current strengths and weaknesses of today's formal specification technology. This provides a basis for formulating a number of requirements for formal specification to become a core software engineering activity in the future. Indirect Use of Formal Methods in Software Engineering Position Statement [PDF] Heinrich Hussmann This position statement points out the advantages of using formal methods indirectly for the development of software. It is admitted that formal methods are not adequate for the daily use in large software development projects, except of a few specialized application areas. However, it is argued that formal methods are well-suited for the analysis of the notions and tools which are used in practice. Examples for indirect use of formal methods are given, including a recent case study on formal foundations for SSADM which was carried out by the author. Retrospective on Formal Methods [PDF] Dick Kieburtz This slide presentation covers the following on formal methods: early work, early work on program transformation, software templates, the DSL experiment: 1993-94, MSL - Message Specification Language, experiment design, aftermath of the DSL experiment, embedded DSL's: experience with HAWK, implementing closed DSL's, program transformation revisited, and programatica Logic - 2001. Seven More Myths of Formal Methods [PDF] Jonathan P. Bowen and Michael G. Hinchey For whatever reason, formal methods remain one of the more contentious techniques in industrial software engineering. Despite great increases in the number of organizations and projects applying formal methods, it is still the case that the vast majority of potential users of formal methods fail to become actual users. A paper by Hall in 1990 examined a number of 'myths' concerning formal methods, assumed by some to be valid. This paper considers a few more beliefs held by many and presents some counter examples. Six Steps Towards Provably Safe Software [PDF] Maritta Heisel This paper presents an approach to the specification and implementation of provably safe software. It uses well-established tools and techniques that are usually employed to ensure correctness, rather than safety, of software. The approach comprises six steps, each of which is complemented by some proof obligations. For each step, the safety-related aspects are clearly elaborated. Thus, designers of safety-critical systems are given guidance that helps to avoid potentially dangerous gaps in the specification of the system's safety properties. Software Engineering with Formal Methods: The Development of a Storm Surge Barrier Control System Revisiting Seven Myths of Formal Methods [PDF] Jan Tretmans, Klaas Wijbrans and Michel Chaudron This slide presentation on formal methods covers the following: the storm surge barrier and BOS, approach to software development, and experiences with the use of formal methods: seven myths of formal methods revisited. The seven myths from "Seven Myths of Formal Methods" by Anthony Hall include: 1. FM guarantee correctness, 2. FM are about program proving, 3. FM are only for safety-critical systems, 4. FM require highly trained mathematicians, 5. FM increase development costs, 6. FM are unacceptable to users, and 7. FM are not used on real software. Back to the top Object Constraint Language (OCL) A DBMS - Based Approach for Automatic Checking of OCL Constraints [PDF] U. Marder, N. Ritter and H.-P. Steiert In large software development projects shared databases support cooperation of developers and reuse of design. Facing complex application requirements and new database technology the development of a corresponding database application is a difficult task. In order to simplify this task, the authors project1 aims at generating the database schema and an object-oriented database application programming interface (API) from a graphically specified UML model. This position paper deals with some very important aspects of our approach: the UML repository (Sect. 2), exploitation of OCL constraints for preserving consistency of both UML models and application data (Sect. 3), and corresponding tool support (Sect. 4). A Semantics for OCL Pre - and Postconditions [PDF] Mark Richters and Martin Gogolla A formal semantics for the Object Constraint Language OCL being part of the Unified Modeling Language UML is described. The authors briefly summarize the semantics of plain OCL expressions which was already presented. OCL expressions are the most important concept in OCL. In addition, they introduce the semantics of pre-and postconditions which rely on OCL expressions but in which some additional language features, like the special variable result in a postcondition, are available. The authors also explicitly define the notions of context and invariant. Automatic Documentation Generation [HTML] Scientific Toolworks, Inc. DocGen automatically generates documentation from Ada or C source code. The content and look of the documentation is specified with a table of content oriented documentation specification. DocGen fills that table of contents. Appendix A Object Constraint Language [PDF] Desmond Francis D'Souza and Alan Cameron Wills This appendix from The Catalysis Approach presents a summary of OCL. OCL in Catalysis is also defined. Appendix B Object Constraint Language [PDF] Author Unknown This appendix introduces and defines the Object Constraint Language (OCL), a formal language to express side-effect-free constraints. The following are discussed: why OCL, where to Use OCL, legend, example class diagram, connection with the UML metamodel, basic values and types, objects and properties, collection operations, predefined OCL, types, and grammar for OCL. Chapter 6 Object Constraint Language Specification [PDF] Author Unknown This chapter introduces and defines the Object Constraint Language (OCL), a formal language to express side-effect-free constraints. Contents include: overview, introduction, relation to the UML metamodel, basic values and types, objects and properties, collection operations, the standard OCL package, predefined OCL types, and grammar. Object Constraint Language Specification Version 1.1 [PDF] Rational Software, Microsoft, Hewlett-Packard, Oracle, Sterling Software, MCI Systemhouse, Unisys, ICON Computing, IntelliCorp, i-Logix, IBM, ObjecTime, Platinum Technology, Ptech, Taskon, Reich Technologies and Softeam This paper on OCL specification contains the following contents: why OCL, where to use OCL, legend, example class diagram, connection with the UML metamodel, basic values and types, objects and properties, collection operations, predefines OCL types, and grammar for OCL. OCL by Example Chapter 4 [PDF] Peter H. Schmitt This slide presentation on Object Constraint Language (OCL) introduces the following topics: the classifier context, the operator context, equivalent notational variations, types (model types, basic types, enumeration types, collection types, special types), subtyping, constraints with associations, constraints and navigation, avoiding allInstances, introducing the iterate operation, quantifiers, and collecting elements. On Formalizing the UML Object Constraint Language OCL [PDF] Mark Richters and Marin Gogolla This paper presents a formal semantics for the Object Constraint Language (OCL) which is part of the Unified Modeling Language (UML) - an emerging standard language and notation for object-oriented analysis and design. In context of information systems modeling, UML class diagrams can be utilized for describing the overall structure, whereas additional integrity constraints and queries are specified with OCL expressions. By using OCL, constraints and queries can be specified in a formal yet comprehensible way. However, the OCL itself is currently defined only in a semi-formal way. Thus the semantics of constraints is in general not precisely defined. The authors approach gives precise meaning to OCL concepts and to some central aspects of UML class models. A formal semantics facilitates verification, validation and simulation of models and helps to improve the quality of models and software designs. Reflections on the Object Constraint Language [PDF] Ali Hamie, Franco Civello , John Howse, Stuart Kent and Richard Mitchell The object Constraint Language (OCL), which forms part of the UML set of modeling notations, is a precise, textual language for expressing constraints that cannot be shown diagrammatically in UML. This paper reflects on a number of aspects of the syntax and semantics of the OCL, and makes proposals for clarification or extension. Specifically, the paper suggests that: the concept of flattening collections of collections is unnecessary, state models should be connectable to class models, defining object creation should be made more convenient, OCL should be based on a 2-valued logic, set subtraction should be covered more fully, and a "let" feature should be introduced. Back to the top