LPSE 2000


"Practical" Formal Methods -- An Oxymoron?

Constance L. Heitmeyer

Center for High Assurance Computer Systems
Naval Research Laboratory (Code 5546)
Washington, DC 20375

Abstract: An important issue in the formal methods community is the degree to
which mathematical sophistication and theorem proving skills should be
needed to apply a formal method in software development. A fundamental
assumption in this talk is that many of the analyses made possible by
formal methods research do not require mathematical sophistication and
theorem proving skills. I will also argue that more ``practical" formal
methods are needed, i.e., methods that have a solid mathematical
foundation but do not require advanced mathematical training. Two
critical attributes of a "practical" formal method are 1) a
user-friendly notation for specifying the required system behavior and
2) a set of tools that detect many classes of errors automatically
and provide feedback useful in error correction. Examples of
additional research (e.g., automatic abstraction methods and automatic
generation of invariants) that can help make current formal methods
more useful in practical software development are proposed. Also
suggested are tool features that would encourage more widespread use
of formal methods by practitioners. To illustrate these ideas, I will
present examples based on the SCR (Software Cost Reduction)
requirements method and describe our experience applying the SCR
method to a number of practical systems.

An Optimal Control System for Automated Synthesis of
Software Systems Using Commodity Objects

Sam M. Daniel

Motorola Inc.

Abstract: The ever-increasing software content in future products, the seemingly
uncontrolled complexity of current development and implementation practices,
the largely unrealized promise of software reuse, and the consequent effects
on timely delivery of reliable and competitive products are all compelling
reasons for pre-emptive action to explore and methodically adopt innovative
approaches that will gradually improve productivity of software based
products by 100X over the next few years. Motivated by the obvious successes
in the hardware industry, encouraged by recent trends in software component
technology, and inspired by the impressive advances in applied constraint
satisfaction, the proposed approach takes the form of an optimal control
system specifically structured to support an adaptively improving software
product development process by making judicious use of prefabricated
commodity objects and guided by intelligent automation to jointly achieve
excellence in technology and success in the marketplace.


Alin-Dumitru Suciu and Tudor Muresan

Technical University of Cluj-Napoca, Department of Computer Science
26-28, George Baritiu St., RO-3400, Cluj-Napoca, Romania

Abstract: One major drawback of logic programming, particularly Prolog, =
is the lack of mechanisms for structuring knowledge (i.e. program =
clauses). This makes programming-in-the-large a difficult task even =
using the module system. Various attempts were made to extend the logic =
programming paradigm with object oriented features. In this paper we =
introduce LOOP, another object oriented extension of Prolog which =
provides object oriented features very similar to those found in =
imperative object oriented languages (e.g. C++, Java), in a very simple =
and straightforward fashion. In LOOP an object is considered to be a =
persistent mutable Prolog term, and therefore, objects can be =
manipulated in a very similar way as classical logic terms. We believe =
that the unique set of LOOP features makes it very suitable for rapid =
prototyping and programming-in-the-large.

Keywords: logic programming, Prolog, object oriented programming, rapid =
prototyping, programming-in-the-large.

Logical Refinement of Imperative Programs: Generating code from verified conditions

Andrew Gravell

Southampton University

Abstract: Most program development methods rely on a combination of
programming and logical notations. Correctness is verified using
refinement laws which often have logical side conditions. Checking
these conditions involves a separate proof, breaking up the linear
flow of the program derivation. This paper explores a variant of
the refinement calculus in which only logical notation is used and
the program under development is inferred from formulas which are,
in effect, the verification conditions that would arise in a
traditional derivation. It is preferable that these are verified
first, in which case they should be called verified conditions. A
polynomial algorithm exists for extracting the refinement argument,
and hence the implementation, from these conditions. A prototype
code generation system has been implemented in Prolog. The benefits
and weaknesses of the approach are compared to those of more
conventional refinement calculi.


Constraint Logic Programming with sets for animation of B formal specifications

Fabrice Bouquet, Bruno Legeard, Fabien Peureux

Laboratoire d'Informatique
Universite de Franche-Comte

Abstract : This paper proposes an approach to the evaluation of B formal specification
s in Set Constraint Logic Programming. For the evaluation of the specifications,
invariant and the pre-conditions with substitution mechanism must be verified
and the graph of reachable states of the specification assessed.

This paper presents a system for constraint resolution to B formal specifications.
This solver is described in terms of constraint domains, consistence verification
and constraint propagation. The constrained state is defined. It was used to
propagate the indeterminism of the specifications and reduce the number of
states in a reachable graph.

The graph exploration was used in animation of specifications. We illustrate this
approach by comparing the constrained states graph exploration with the valued
one in a simple example: Process scheduler.

Key words : B Method, Evaluation of specifications, Animation, CLP, CSP, Set constraints

Server Side Web Scripting in Curry

Michael Hanus

University of Kiel,

Abstract: In this paper we propose a new approach to implement web services
based on the Common Gateway Interface (CGI). Since we use the
multi-paradigm declarative language Curry as an implementation
language, many of the drawbacks and pitfalls of traditional CGI
programming can be avoided. For instance, the syntactical details of
HTML and passing values with CGI are hidden by a wrapper that executes
abstract HTML forms by translating them into concrete HTML code. This
leads to a high-level approach to server side web service programming
where notions like event handlers, state variables and control of
interactions are available. Thanks to the use of a functional logic
language, we can structure our approach as an embedded domain specific
language where the functional and logic programming features of the
host language are exploited to abstract from details and frequent
errors in standard CGI programming.

The Role of Logic Programming in Next-Generation Component-Based Software Development

Kung-Kiu Lau

University of Manchester, UK

Abstract: To date Logic Programming has not made any impact on Software
Engineering. As Software Engineering moves on from objects to
components, will Logic Programming be simply forgotten forever? In this
position paper, I will argue that the answer could be and should be, perhaps
surprisingly, negative.

Optimisation problems in logic programming: an algebraic approach

Silvija Seres and Shin-Cheng Mu

Oxford University Computing Laboratory
Wolfson Building, Parks Road
Oxford OX1 3QD. U.K.

Abstract: Declarative programming, with its mathematical
underpinning, was aimed to simplify rigorous reasoning
about programs. For functional programs, an algebraic
calculus of relations has previously been applied to
optimisation problems to derive efficient greedy or
dynamic programs from the corresponding inefficient but
obviously correct specifications. Here we argue that this
approach is natural also in the logic programming setting.

A Software Engineering Methodology based on Logic Programming}

Gopal Gupta

New Mexico State University

Abstract: In this paper we investigate how logic programming technology
can aid software development. Two approaches are discussed. In the
first approach, given a program written in a traditional language
(e.g., C), an equivalent logic program is automatically obtained.
This equivalent logic program serves as a high level abstraction
of the original program and can be put to a number of uses including
debugging and code generation. The second approach is centered around
domain specific languages. Given a task for which a software system is
to be developed, a high-level domain specific language is first designed.
Domain experts can use this DSL for writing programs at their level
of abstraction. Logic programming provides a framework in which programs
written in this DSL can be interpreted, compiled, debugged,
and profiled.

AUTOFOCUS on Constraint Logic Programming

Heiko Loetzbeyer and Alexander Pretschner

Institut fur Informatik
TU Muenchen

Abstract: The CASE tool AUTOFOCUS allows for modeling and validating
reactive systems on the basis of a simple, clearly defined formal semantics.
It is shown how executable code for common CLP languages can be generated
automatically. Aplicaitons include simulation for rapid prototyping
and debugging as well as semi-automatic generation of test-sequences.