Processes and Tools for Formal Approaches to Development
                        Working Group

Introduction  (Betty Cheng):

What are tools and processes needed to support formal
methods?
- Industrial strength tools?
- Scalable FM processes
- Industrial case studies
- Future research

Open issues:
- criteria for industrial strength tools/processes
- Application dependent/independent tools/processes
- Certification of software?
- Certification of software engineers?

Types of processes:
- Informal
- Semi-formal (specifications, clean room)
- Formal

FM Tools that support:
- Reuse
- Analysis
- Design
- Testing
- Reverse/Re-engineering

Where does the CMM fit?
- What type of metric does it offer?
- How useful is it?
- Who uses it now and why?
- Should more/different information be evaluated?
:
Questions to be addressed:
- What is a process?
- What are types of processes?
- What is a FM process?
- What is a tool?
- What are techniques?

Process Definition and Discussion:
Break into groups of 2 to develop a definition of what a process
is:
G1:
- process need not necessarily terminate
- inputs permitted throughout, not limited to beginning only
- output can include reusable resources (libraries, etc.)

G2:  an ordered set of well-defined tasks each with a
beginning and end, each task has a metric to measure
performance (ask for clarification)

G3:  a set of interrelated activities related to creation of
software

G4:  a partial ordering of tasks with time/cost/resources
constraints, achieving a goal, should be part of a larger
system as a whole, not just the software

could have a hierarchy of processes (s/w develop process
inside of system development process, etc.)

Example:  Fagan Inspections:
planning --> overview --> preparation --> meeting --> rework
--> follow-up


sequential, get a metric out, output:  better document

Process definition:
- a set of interrelated tasks
- each task has input/output
- there is a specific objective for the interrelated tasks
- there exists a metric to evaluate each task
- set of tasks that can be replicated

FM Process:
If you use FMs you should get something out that is
verifiable (set of requirements?  other things?)
What is the output of a FM process?
A FM process is a process that employs FMs.


 How FMs fit within the life cycle:

Divide into groups again to discuss FM process:

G1: FMs may not change the overall steps in the s/w
development lifecycle, may add some steps;
takes what is implicitly done by programmers and makes it
explicit;
FMs can be added any place in the life cycle process

G2:  process definition is not different, but apply FMs to each of
the tasks, can possibly eliminate tasks through automation;
can help construction of product, not just verifying

G3:  product model and process model, can have
formal/informal model for each - V doesn't change, what goes
in the boxes does change

Most life cycles are management structures and beat up the
product, stage tends to be defect generators because
of the involvement of humans.  Formal methods process
throughout the life cycle.
Issues:  is the FM process people intensive?  Can it be
automated?  Can it be reduced?








V-model for Development Process:


Break into groups again to discuss:
What are the techniques are needed to use FMs in each box of
the V lifecycle diagram?  What
near term goals can we expect to see achieved to use FMs in
each box.  What about long term goals?

Summary:

Requirements:  Use of a formal notation to get the
requirements down, also executable spec.  constraint
management, consistency checking

Tech design:  simulatable specs, theory based design

Detailed design:  formal refinement techniques, formal
architectures

Coding:  formal synthesis techniques, verifying compilers
and compilation

Integration:  protocol verification, APIs, proofs of
composition, process algebras

System:  heterogeneous specification techniques

Acceptance:  automatic test pattern generation


Acceptance testing may be a relaxed form of the
requirements.
Requirements drive the acceptance criteria.

As of today, we have techniques supporting FMs at boxes:
- Detailed Design





Tool Support for Techniques:

Where are we now in terms of tools supporting FM techniques,
and where do we want to go?  What kind of tools do we need
to see at each box, and who are the intended users of the
tools?  How can the use of FMs be increased?

Suggestions:
     - Education:
          - teach it to undergraduates systematically;
          - develop course materials (textbooks, lecture
materials) for undergraduate courses in the         context
of OO paradigms and FMs (Intro, Data Structures, Operating
Systems, etc.);
          - find a way to make FMs as fun and popular as C++
is today (write a book for FM in               the same
spirit as the book Internet for Dummies book),
     - Tool Needs: develop tools that are easily usable by
programmers who are not PhDs.

Tool Needs:

Break into groups to discuss:  techniques for going from the
Detailed Design box to the Code box in the V model:

G1:  techniques - vertical:  design written in formal lang.
with a semantic, refine it by stages (introducing new
issues, fleshing out issues) compare each successive version
to ensure the semantics remain the same, then generate code
automatically; horizontal:  simulation, test suites, formal
analysis and proofs (helps with V&V)

G2:  techniques - derivation (weakest preconditions),
transformational, compilation (moving from spec directly to
code, like from Z to C++), successive refinement (have to be
very careful at each step, may have a proof obligation at
each step)

May need to find ways to restrict domains of units within
tools to make outputs efficient enough.

G3:  Techniques -
Requirements box - model checking, temporal logic
Technical design box - process algebras, pre/post conditions
Detailed design box - pre/post conditions, optimization
tools (to get good code)

G4:  techniques - transformation (KIDS, Specware),
deduction, calculation, verification (model checking,
theorem proving)

What tools:
     Do we have in academia, in industry?
     What tools can we modify?
     What tools (i.e. functionality) do we need?

Break into groups to discuss:  what functionalities are
needed in tools to support the techniques arrived at in the
previous discussion

G1:  Refinement:
-    build theories (vocabulary and a set of assumptions
  about vocabulary, or language and as set of axioms)
-    theory morphisms

     tools: KIDS - has generic refinements but weak on
     theorem proving, IMPS - strong on theorem proving
G1:  horizontal - deductive analysis; vertical - build a
language of design building blocks and assemble design from
the building blocks
)
     

G2:  Derivation:
-    appropriate representation (specification language with
  good semantics, can do expression simplification, has a way
  to calculate weakest preconditions, can suggest possible
  code structures)

     tools:  none known available (maybe Penelope?)


Transformation:
-    Coherent rule base, large enough to do real problems,
  comprehensive, can take a spec and generate efficient code
  (rewrite rules), correctness-preserving rules

Refinement:
-    theorem prover to verify each refining step (rules are
  not necessarily correctness-preserving, youre adding
  meaning as you go along)
-    Refining step generation can be anything from manual to
  completely automated

Compilation:
-    parsing techniques for specs
-    appropriate intermediate language

G3:  functionality needed - transforms one language into
another

G4:  Need a user-friendly, robust theorem proving system
(theorem prover can say:  theorem is true, or I dont know -
need to give user help with what it means when the theorem
prover says "I don't know")
Need support environment: config management, library
services, help you write theories (consistency checking,
etc.), support for heterogeneity (don't want to have to use
transformers)

Break into groups to discuss:  techniques to go from
Requirement box to Design, then functionalities needed for
tools

G2:  Requirements gathering is very important, but no good
tools available.  Observation of user/customer
interactions/behavior can be very important.  Need models
for what you're working against - context, domain,
individual.  Process algebras

G4:  Moving from a description of what to a description of how,
transforming a model, but harder than going from design to
code because there is no source model.  Executable
specifications, and maybe rapid prototyping.  Very high
level model checking.

G3:  Observation.:  many engineers skip the requirement step
and plunge directly into design.
To go from requirements to design, need transformations, but
problem is that transformations are known for specific
domains.  Process algebras are good for transformations.

Day 2:

Deliverables/Tangible Products for Presentation:

-    Presenters: Perry Alexander (Acad); Bill Farmer
  (Industry)
-    Status report:
     -    Discussions
     -    Findings
-    Future Activities
-    Discussion:
     -    Process Definition
     -    FM Processes
     -    V-model
-    Techniques to support FM
-    Tools to support techniques
-    Findings:
     -    Future directions
          -    Education
          -    User-friendly tools
-    Tools with simulation, not just verification
     -    Short term vs long term goals for techniques and tool
     development to support FMs in the boxes in the V model