http://swarm.wustl.edu/ (World Wide Web Directory, 06/1995)
The Concurrent Systems Group
People
Purpose
The Concurrent Systems Group (CSG) seeks to develop practical methods
for the specification and design of dependable concurrent systems
supporting critical applications. The emphasis is on methodological
advances that extend the applicability of formal program derivation
techniques to industrial-grade problems. Program visualization serves
to make formal concepts accessible to a broad audience. We also hope
that insights gained through this research will contribute to a better
understanding of how to teach formal methods to future generations of
software designers.
Research Environment and Background Information
Reseach Agenda
Formal Design Methods
- Develop techniques for modular specification, design, and
verification of highly mobile computations, i.e., systems consisting
of large numbers of programs which move in space and change their
communication patterns in a location dependent manner; this involves
introducing the notions of transiently-shared variables and actions
and a reevaluation of the UNITY-style composition (union and
superposition)
- Demonstrate that program specification, design, and verification
techniques originally developed for computing with tuplespaces can
provide a formal underpinning for reasoning about cooperative work
- Develop strategies for the design of very large, fault tolerant,
correct-by-construction systems out of simple trusted intelligent
components; one possible application is the design of rail traffic
control systems
Program Visualization
- Complete the deployment of a new version of
Pavane ; new look,
simpler interface, more distributed, more interactive, more flexible
to use
- Demonstrate that declarative visualization and Pavane can deliver
industrial-grade, distributed, end-user applications with minimal
programming effort
Recent Results
Formal Design Methods
- Extended the UNITY notation and proof logic to concurrent
computations over tuplespaces (the Swarm model)
- Introduced formal verification and program derivation techniques
to concurrent rule-based programming
- Showed that architectural constraints can be specified as
assertions in the UNITY logic and developed techniques for using
formally stated architectural constraints in program derivation
- Explored practical ways to integrate specification and program
refinement
Program Visualization
- Pioneered the use of declarative visualization, a technique which
allows one to specify complex visualizations by simply writing sets of
rules which map prgram states to full-color, three-dimensional,
animated images
- Built, refined, and evaluated Pavane, the first program
visualization system to exploit the capabilities of declarative
visualization
- Demonstrated the applicability of program visualization to a
broad range of applications including teaching concurrent algorithms,
scientific visualization, rapid prototyping, requirements validation,
software monitoring and debugging
Last updated: Dec 12 1994
http://swarm.wustl.edu/ (World Wide Web Directory, 06/1995)