Working Group on

Support for Teaching and Learning Formal Methods

Version: Monday evening at 1715

 

WG Members:  

Vicki L. Almstrum (co-chair)

University of Texas at Austin

C. Neville Dean (co-chair)

Anglia Polytechnic University

Tom Hilburn

Embry-Riddle Aeronautical University

Don Goelman

Villanova University

David Gries

University of Georgia

 

Advisory Board Members:  

Jonathan Bowen  

South Bank University

Dan Craigen

ORA Canada

Kathi Fisler

Rice University

Susan Gerhart

Embry-Riddle Aeronautical University

Ebba Thora Hvannberg

University of Iceland

D. Randolph Johnson

National Security Agency

Peter Gorm Larsen

IFAD A/S

J Strother Moore

University of Texas at Austin

Lesley Semmens

Leeds Metropolitan University

Jan Smith

Chalmers University of Technology

Moshe Vardi

Rice University

Jeannette M. Wing

Carnegie Mellon University

J. C. P. Woodcock

Oxford University Software Engineering Centre

 

Goal:  Make it natural (and obvious) for the computing education community to incorporate formal methods as a key aspect of the curriculum.

 

The ideal is to have folks incorporate  formal methods without even realizing it!!

 

Closing the Gap

formal

methodists

computing
educators

illustration of gap between

Problems and Challenges

What are Formal Methods?

  Group’s general working definition (derived from the below ideas about formal methods and the goal of our group):

  Some definitions drawn from various sources:

·        “The use of mathematics to aid in software development is known as formal methods.”
D.C. Ince -       An Introduction to Discrete Mathematics, Formal System Specification, Z, Oxford, 1992.

·        “By formal methods I mean the specification and verification of hardware and software systems.”
Jeannette M. Wing, Weaving Formal Methods into the Undergraduate Computer Science Curriculum, Proceedings of the 8th International Conference on Algebraic Methodology and Software Technology, May, 2000.

·        “A broad view of formal methods includes all applications of (primarily) discrete mathematics to software engineering problems.  This application usually involves modeling and analysis where the models and analysis procedures are derived from or defined by an underlying mathematically-precise foundation.”
N.G. Levenson, “Guest Editor's Introduction: Formal methods in Software Engineering”, IEEE Transactions in Software Engineering, September 1990.

·        “... that body of theory, techniques, pedagogy, and tools that enable rigorous reasoning reasoning in system design practice.”  http://www.cs.indiana.edu.formal-methods-education/xxiee/report.html

·        “A formal method in software development is a method that provides a formal language for describing a software artifact (e.g. specifications, designs, source code) such that formal proofs are possible, in principle, about properties of the artifact so expressed.”  Robert Vienneau, A Review of Formal Methods, Kaman Sciences Corporation, 1993.

·        “Formal methods can be roughly divided into basic components: specification and verification.
Formal specification is the use of notations derived from formal logic to:
  1. describe the assumptions about the world in which a system will operate;
  2. the requirements that the system is to achieve;
  3. a design to accomplish those requirements.
Formal verification is the use of proof methods from formal logic to:
  1. analyze specifications for certain forms of consistency and completeness;
  2. prove that the design will satisfy the requirements, given the assumptions;
  3. prove that a more detailed design implements a more abstract one.
The mathematics of formal methods include:
  1. predicate calculus (order logic)
  2. recursive function theory
  3. lambda calculus
  4. programming language semantics”
                        http://ntsta.jrc.it/dsa/vse/fm1.html

·        "My approach to software has been that of a study in management, dealing with a very difficult and creative process.  The first step in such an approach is to discover what is teachable, in order to be able to manage it.  If it cannot be taught, it cannot be managed as an organized, coordinated activity.  Since software deals with purely logical processes, it seemed clear that mathematics was the right tool to apply to the problem.  In this search for teachability, it has been a pleasant surprise to find that so much of software methodology could be formulated in classical mathematics.”  Harlan Mills - Software Productivity(p. 2), Dorset, 1988.

  What is your view of Formal Methods?

Formal Methods in Computing Curricula ’91 and Computing Curriculum 2001

Don Goelman is working up the matrix and survey for looking at this issue.

 

Formal Methods in Software Engineering

Tom Hilburn is working on a summary of this.

Framework for a “Getting Started” Resource on the Web

Help in “Taking the next step” (not just getting started)

Building on an existing web site

Some suggestions for what should be incorporated

 

Concept Map for Formal Methods

This will be a large poster section with “Formal Methods” in the middle, a line dividing the plane into “Applications” and “Concepts”.  We will seed the page with some points:

Our goal is to have the attendees help fill in other points and perhaps even to somehow vote on what should be included.