ASSESS is supported by NWO-GBE project number 612.062.000.

Contact Address:
Adriaan de Groot
Informatica / ITT
Room A6020
Toernooiveld 1
Nijmegen, the Netherlands.
Tel. +31 24 36 52272

The ASSESS (Architectures for the Structured Specification of Embedded Systems Software) project aims to find or build architectures for software specification and evaluate those architectures. In addition, it aims to articulate what is fundamental to architectures for system specification, i.e. what makes a particular architecture "good" or "useful" and applicable to a particular problem.

The project aims to both develop (our own) and evaluate (our own and others') tools and methods for the construction of requirements documents -- a crucial part of the software production process. These requirements documents can be considered the first step to the specification of the system. By producing structured requirements documents through a well-defined formal process, we hope to improve the quality of these documents and hence of the software as a whole.

The final goal of the project is to be able to evaluate methods and tools effectively based on fundamental notions of what is useful and necessary for writing requirements documents. To this end we will be developing tools and methods and applying them to case studies. In addition, we will evaluate tools and methods from outside sources. We should be able to say "this is what makes a tool (or method) good, and tool X is good (or bad) by this criterium."

The project will proceed through two main phases: that of experimentation (doing case studies) and that of analysis (finding out what made each case study easy or difficult).

Experimentation Phase: In the experimentation phase we select case studies -- perferably fairly small documents describing a software system -- and a method (possibly tools as well) in order to get some experience in applying the method. This phase has the following case-studies, at the very least:

• The light control (2000).
• The BART study (2001,2002).
• The MARS study (2003).
• The light control, re-done with the LSC tool from the MARS study (2003).

This phase collects concrete results. The primary result of each study is the report on the errors found in the informal specification and how these are resolved. The secondary result is the evaluation of the method or tool used. No particular effort is made to correlate results, although experiences and improvements in tools are obviously carried over.

Analysis Phase: In the analysis phase we will try to distill the evaluations of the various tools into recommendations wrt. the tools themselves and into criteria for evaluating other tools. This phase should start in september 2003.

The ASSESS Project aims to develop a method that uses formal notation for the improvement of requirements documents. We begin with an informal requirements document couched in some natural language -- typically English. Our method translates this document in part into semi-formal notations like the UML, and from there into formal notations like the logic of the PVS theorem prover. The translation done requires a good deal of understanding of the terminology of the informal document and usually uncovers a great deal of inconsistency in the use of terms and the requirements. The formal notation can be analyzed with the PVS tool. This lets us deduce behavior and prove proerties of the formalized system. These results can be used to adjust and modify the original informal specification.

We believe that performing this kind of analysis and adjustment improves the quality of the original informal specification. In addition, the semi-formal and formal documents we produce are in-sync with the informal document and useful for further software development work.

The first case study of the project, the Light Control, was a case in which the analysis of the formalized requirements yielded a number of subtle incompatibilities. The second case study, on the BART system, had a complex operating environmented which needed to be understood (and which was poorly described in the informal document) before any system design could be done.

Our next study aims to our focus to evaluation. The first two studies served to make the method concrete and determine what we believe is a fruitful approach. In this new study we will first spend some time becoming acquainted with new tools: TAME, and some Live-Sequence Charts tools as well. Then we will formulate a hypothesis relating to the usefulness of the tools in performing the formalization of a new informal document following our method. This formalization period will have a strict time limit. Afterwards, we can evaluate the usefulness of these specific tools in the case study.

This somewhat "experimental" approach -- in the sense that we experiment with various tools and approaches -- is intended to provide us with some concrete data on the applicability of the tools that are used in the specific area of the case study. This is intended to make it possible to choose a tool sensibly for a given task. Currently it seems like everyone and his dog is creating tools, inventing formalisms, etc., for some specific purpose, but very little is done in applying tools outside of the particular domain in which they are conceived. In a sense, we wish to provide a "shopping guide" for tools in the sense that Freek Wiedijk has done for proof-checking tools.

The Light Control Case Study was a case study for a special issue of the Journal of Universal Computing Science. The study consisted of applying our favorite formal method -- our automaton framework (mentioned below) in an earlier incarnation -- to the problem of automating the lighting system in a university building.

Our results, based on a careful sentence-by-sentence translation of the requirements stated in the informal document, show that the requirements are inconsistent.

Current status: Finished, published.

Importance: This is a short and simple study that shows off some PVS approaches to demonstrating inconsistency in requirements.

The Bay Area Rapid Transit system is the light rail system in the San Fransisco area. This case study was similar to the Light Control: apply your favorite formal method to an informal document. We applied our automaton framework again, refining it considerably in the process. In this study, the requirements were fairly straightforward, but the model of the environment was complex. Proving the simple safety properties of the total model was complicated by the complex dynamics of the environment.

Our results were a model and a proof of the safety thereof. The model neglects many aspects of the real system. This could be corrected, but probably at the expense of even more tedious algebraic manipulation in PVS.

Current status: Finished, published.

Importance: This study shows how timing and dynamics can be introduced into the automaton framework.

The automaton framework is a collection of theories in PVS related to (Hybrid) automata. The purpose of the framework is to make it relatively easy to write automaton descriptions in PVS and to prove properties of the automaton. It is similar in intention to TAME, but much less ambitious. As a consequence, the automaton framework will probably be easier to understand as a whole and better documented.

This work consists of two parts:

• The framework itself in PVS, consisting of theories and support lemmas. We avoid using strategies or tactics since these are not visible in the same scope as the theories.
• Documentation and examples of how to use the framework. We have "given" this framework to a number of PhD students to work with, and it seems that ythe learning curve is very steep when both PVS and automata need to be dealt with simultaneously. Therefore we need a few good examples of "proper style" so that the amount of PVS that needs to be remembered is minimized.

Current status: The theory is in place but missing many support lemmas. There are a few tutorials but no unified document on how to use the framework.

Importance: The automaton framework is the semantic basis for all of our case studies.

This case study intends to use the Play Engine tool developed by Hillel Kugler and David Harel (and others). The purpose is to quickly learn to use the tool and check whether all the different error codes defined in the MARS document are "compatible," in the sense that the requirements don't demand two different behaviors at the same time.

Current status: Just starting, and a little disappointed in the tool. It's got lots of front-loaded stuff before you can use it (and I need to learn VB, too). This is scheduled to be drawn up (on paper) at the beginning of february.

Importance: Evaluating external tools is important in developing criteria for excellence that extend beyond our own little PVS theories.

This is intenden to be a very small case, just as an exercise in LSC construction on paper of requirements I already know fairly well.

Current status: Nothing yet. Scheduled for the week of january 27th.

Importance: No much, but it will show how different approaches -- different architectures for representing requirements -- can highlight different aspects of an informal requirements document.

The research project started in 1999, with a one-year funded research contract from ICT, the Dutch IT company. That project was called FRESCoS (Formal Requirements Engineering in a Commercial Setting) and was intended to do something resembling RE with commercial products. Unfortunately, not much came of the project besides the LCCS. Working together with an industrial partner that's a long way away is a tricky business.

In 2000, the project funding was taken over by NWO, under contract 612.062.000 with project title ASSESS (Architectures for the Structured Specification of Embessed Systems Software). This was to be a 3-year post-doc project, but -- since I'm still pre-doc -- it got turned into a 4-year PhD. project. The purpose of the ASSESS project is similar to that of the original FRESCoS: implement and evaluate formal methods for requirements specification.

Last changed Thu Jan 29 14:17:57 MET 2004