A new blog ... visit OnCenter, Roger Pressman's running commentary on the world at large
A new edition ... the 6th edition of Software Engineering is available now
A first novel ... Roger Pressman's first novel is a technothriller -- The Aymara Bridge
A new training curriculum! RSP&A has partnered with QAI to develop a comprehensive Internet-based software engineering curriculum.
A redesigned Web site ... we've done a major redesign and added many new features
This page provides access to a variety of downloadable papers that
address formal methods issues. The following topics are considered:
Object Constraint Language (OCL)
An Introduction to Z and Formal Specifications [PDF]
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]
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]
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]
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
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.
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.
Object Constraint Language [PDF]
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.
Object Constraint Language Specification [PDF]
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,
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
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