VERIFICATION ALGORITHM RESEARCH GROUP

(Most recent essential modification 2001-09-10)
(Most recent modification 2001-09-10)

  1. Introduction
  2. History
  3. Research Themes and Results
  4. ARA Toolset
  5. Members
  6. Funding
  7. Research Co-Operation
  8. Links to Relevant Topics
  9. Publications by the Group 1993-
  10. Other References

1. Introduction

This document introduces the Verification Algorithm Research Group working in the Institute of Software Systems of the Department of Information Technology of Tampere University of Technology. A slightly modified paper version of this document as of summer 1996 was published in [96-5].

To get a feeling of our field, we recommend the reader to look also at [96-1] (HTML version here). It gives a non-technical introduction to a verification approach utilising our results. One should notice, however, that it discusses only the very basic approach, and its tool section is out of date.

Goal of the Group

The goal of the group is to develop

for computer-aided verification of computer and software systems. The group concentrates on reactive and concurrent systems.

Reactive and Concurrent Systems - What are They?

A system is reactive if it is in continuous interaction with its environment. A system is concurrent if it consists of several conceptually autonomous but co-operating units. The units are often called processes. Reactive systems are usually concurrent.

Telecommunication protocols and computers embedded in electronic products (cameras, elevators, mobile phones, . . . ) are important application areas for results concerning reactive systems.

Formal Models and Specification Formalisms

The verification of "real" software such as C or Ada code is far beyond the current state of the art. Therefore, the object of verification is always a formal model of the system written in some abstract specification formalism.

From the vast variety of specification formalisms suggested so far the group uses mainly (representations of) labelled transition systems (LTS), and sometimes Lotos [BoB87, ISO89] (see 8. Links to Relevant Topics).

Labelled transition systems are graph-like representations of (global) behaviours of systems. They resemble and can be interpreted almost like finite state machines. The main differences are that there are no acceptance states, and invisible moves have a different interpretation. Furthermore, several operators have been defined for transforming LTSs and composing several LTSs together that do not have counterparts in the classic theory of finite automata.

Lotos is a formal specification language standardised by ISO. It is intended for the specification of the behaviours of distributed and reactive systems, in particular protocols for the Open Systems Interconnection model.

Below is an example of Lotos code and the corresponding LTS.

process Receiver[ rec, dat, ack ]( sn : seq_nr ) :=
  (* receive message from channel *)
  dat ? sr : seq_nr;
  (  (* correct seq. nr. -> deliver and ack *)
     [ sn = sr ]-> rec; ack ! sr;
     Receiver[ rec, dat, ack ]( sn+1 )
  [] (* incorrect seq. nr. -> acknowledge *)
     [ sn /= sr ]-> ack ! sr; Receiver[ rec, dat, ack ]( sn )
  )
endproc
A picture of an LTS

What is Verified

Formal verification requires also that we specify what properties the system should have in order to pass. The properties may be general, such as absence of deadlocks, or system-specific, such as "if the call button at floor 7 is pressed, then the lift should eventually be standing doors open at floor 7".

The group is interested in the verification of both kinds of properties. In particular, we are interested in verifying systems by comparing them to other systems according to some formal criterion. For instance, a formal model of a protocol may be verified by formally checking that it behaves in the same way as a formal model of the corresponding service specification. We are also interested in verification (or validation) by visualisation, that is, by manual inspection of a computer-generated graphical LTS representation of chosen aspects of the behaviour of the system.

Theoretical Background

From the above it is apparent that a great deal of the work of the group follows the process-algebraic tradition (e.g. [Hoa85, Mil89], Ros98]). However, our emphasis is on algorithms, not on process algebras. We are willing to apply our ideas to and learn from other domains, too, such as temporal logics [MaP92, Eme90], Petri nets [Mur89, Jen92], and DisCo-style action systems [BaK88, KJ+90] (see 8. Links to Relevant Topics).

The main technique adopted by the group is state space analysis. That is, the system under analysis is simulated to (a representative set of) all the states it can reach. Of course, all except some trivial systems have much larger state spaces than can be handled in a realistic computer. This problem is known as state explosion. Perhaps the most important results of the group deal with the verification of systems by investigating only a small, carefully chosen subset of reachable states (see 3. Research Themes and Results). An LTS, by the way, is just one kind of a state space that is suitable for the process-algebraic framework.

The chapter [98-4] is an extensive tutorial to the field of verification with state space analysis. It covers most if not all basic ideas and, discusses many advanced techniques.

Tools

As a test bed for our ideas we have used the ARA toolset [KL+92, 93-1, 95-3]. ARA can be used for analysing and comparing the behaviours of models written in Lotos. Although ARA was originally not developed at Tampere University of Technology, it has common roots with the group (see 2. History). Furthermore, the group has developed new tools and uses also them (see 3. Research Themes and Results, subsection Tools). It is anticipated that the group will gradually move from ARA to an entirely new set of tools during 2000-2001.

2. History

The group has its roots in the "RIMST" research project conducted during 1984-1988 at Helsinki University of Technology and the Computer Technology Laboratory of the Technical Research Centre of Finland (currently VTT Electronics) (links to these in 7. Research Co-Operation). The goal of RIMST was to develop Petri Net -based tools for the analysis and verification of concurrent systems. During 1989 VTT Electronics changed its focus into verification methods based on process algebraic theories. Research was continued in the ARA (1990-1992) and AATOS (1992-1995) projects. In addition to a number of publications and other scientific results, these projects produced a verification toolset called ARA (see 4. ARA Toolset).

In the middle of 1992 Antti Valmari (see 5. Members), who had joined the RIMST project 1985 and had been one of the key verification researchers in VTT Electronics, moved to Tampere University of Technology, Software Systems Laboratory (SSL) (now called "Institute of Software Systems"). This started a period of close research co-operation between SSL and VTT Electronics. In the beginning of 1993 VTT Electronics was accepted as a partner into the European Union ESPRIT III Basic Research project #6021 REACT: Building Correct Reactive Systems [Wol93] (link in 7. Research Co-Operation), and Valmari was nominated as VTT's representative in it.

The Verification Algorithm Research Group at SSL was born (not established!) Jan. 1, 1994, when SSL and VTT Electronics made their first research contract. Since then the group has been slowly growing. Because verification research had not reached the maturity level required for large-scale industrial application, VTT Electronics decided not to continue it after AATOS ended in the middle of 1995. This led to the shift of the responsibility of research on verification algorithms and of the maintenance of the ARA toolset to SSL.

3. Research Themes and Results

The group is interested in both developing verification theory and testing its practicality by conducting small-scale case studies. Below we describe briefly the main results we have obtained classified (somewhat arbitrarily) into some themes. Bibliographic information of the publications cited below is found in 9. Publications by the Group 1993-.

Verification Methodology and Verification Case Studies

A non-technical overall introduction to process-algebraic verification in general and our approach in particular was given in [96-1], available also in HTML form. The paper discusses only the basic approach and skips the more advanced techniques. The invited talk [96-4] describes process-algebraic verification at a slightly more technical level. It introduces the most important process-algebraic semantic models and fundamental algorithms for manipulating labelled transition systems (LTSs) according to them. The tutorial [00-4] has been written for users of LTS-based process-algebraic verification. Its emphasis is on the construction of system from LTSs, compositional analysis, and our favourite semantic model. It discusses in detail a case study, where an infinite family of demand-driven token-ring systems is verified with a finite amount of effort.

The first papers describing the use of the ARA toolset in verification were [KL+92] and [93-1].

Around 1993 ARA was expanded by the addition of a visualisation tool. It can show small LTSs on a computer screen in a readable form. We soon realised that visualised suitably pre-processed LTSs give the system designer extremely useful feedback from the behaviour of his design. We tested this idea in the validation of Peterson's well-known mutual exclusion algorithm in [94-3].

Visualisation of LTSs started to seem to us as a good way of obtaining feedback during system design. We tested its usefulness by developing an advanced version of the alternating bit protocol [96-2]. The improved protocol tries retransmission only a finite number of times, and contains a mechanism for synchronising the alternating bits of the sender and receiver whenever necessary. Such synchronisation is needed when the maximum number of retransmissions has been made without success. This work was continued in [97-2] by investigating bidirectional (or full-duplex) protocols.

In [96-3] we studied the problems encountered in the verification of progress (also called "liveness") properties using process-algebraic approach and visualisation. The paper contains a more careful analysis of Peterson's algorithm than [94-3]. With an innovative application of so-called "compositionality", in [98-1] we were able to take so-called fairness assumptions into account during verification. Fairness assumptions are often crucial for proving that a system makes progress, and their handling has been a difficult problem for process-algebraic methods. More details of this will be given in Compositional state space generation below.

Another way of handling progress was developed in [00-3]. A fairness assumption was represented as an infinite LTS. For automatic verification, this LTS was approximated from below and above by a finite LTS. In this way two behaviours were obtained, from which the real behaviour of the system could be easily reasoned.

A new direction in visual verification was opened in [00-5]. In it, a method for visualising an interesting part of the behaviour in greater detail than other parts was developed. The method can be used to find out reasons for livelocks, for instance.

A case study that was larger than the ones mentioned above is reported in [96-6, 96-8]. In it, we used visualisation during the development of a simple add-on protocol for the Ethernet. The goal of the protocol is to control access to the Ethernet in such a way that collisions are avoided.

Process-Algebraic Semantic Models

As was already mentioned, [96-4] is a tutorial or survey that covers the most important semantic models and algorithms for them. Also [98-4] contains information on the most widely known semantic models and algorithms.

The choice of the semantic model that is used in process-algebraic verification determines what properties can be verified and what kind of techniques for alleviating the state explosion can be used. The group has found out that contrary to a common belief, the state explosion problem can be best managed if the equivalence is as weak as the verification task allows. These issues are analysed in detail in [95-2], and later in a wider context in [98-4]. Bill Roscoe from Oxford University Computing Laboratory (a key person in the development of tools [Ros94] for the famous CSP theory of Brookes, Hoare and Roscoe [BHR84, BrR85, Hoa85, Ros98]) said about [95-2] in an email message (cited with his permission): "The title of the last paper you suggest is most apt. I was put off tool-building for CSP for several years by the knowledge of the complexity results lurking in the background, until at last I was forced to think about it in 1990/1 and invented the algorithms that FDR runs, usually linear in the state-space."

Together with its collaborators, the group has found the weakest possible semantic models for the verification of certain important classes of properties [VaT91, KaV92], [95-5, 95-1], [99-1].

In its work the group uses mostly the Chaos-Free Failures Divergences semantics (CFFD) [VaT91], [95-5]. It resembles the well-known CSP semantics by Brookes, Hoare and Roscoe, but does not suffer from the "catastrophic divergence" problem of CSP. One reason for choosing it was that it is the weakest possible compositional semantic model that preserves both all the properties specifiable in "nextstate"-less state-based linear temporal logic and deadlocks [KaV92]. Roscoe has given credit on this work and some other parts of our work in his new CSP textbook [Ros98 p. xv, 216, 243, 464, 529]. In 1999 Valmari was invited to give a talk on CFFD-semantics at a seminar held In Celebration of the work of Tony Hoare on the occasion of his retirement, and later write an article [00-6] for a book based on the talks in the seminar. Sir Tony Hoare is one of the most famous researchers in computer science and the 1980 winner of the Turing Award. The seminar speakers included six other Turing Award winners.

The handling of data aspects of systems during verification with state spaces is a very big problem. Its most general form is clearly undecidable. Because data aspects sometimes affect concurrency aspects, it is sometimes necessary to include a small amount of data aspects in a verification model. The traditional way of doing that is unfolding, that is, explicit representation of all data values in the global state of the system. However, unfolding causes serious performance problems to state space methods. The paper [97-3] and theses [97-6] and [98-3] present a way of adding data and its manipulation to LTSs (a certain kind of state spaces) in a symbolic form. The idea is that symbolic data is kept uninterpreted until late stages of verification. It is eventually unfolded, but only at a stage where it does not cause too much state explosion. Furthermore, sometimes it is possible to keep it uninterpreted.

Although the group concentrates on the CFFD semantics, other semantic models are not forgotten. The problem of minimising the number of transitions of a state-minimal LTS with respect to observation equivalence and branching bisimilarity when divergences are / are not preserved is solved in [97-5].

Techniques for Alleviating the State Explosion Problem

The expertise of the group in the state explosion problem received international acknowledgement, when Valmari was asked to write a 100-page introduction to it [98-4].

Valmari was among the first to investigate so-called partial-order verification methods when he developed the first version of the stubborn set method in 1988 (e.g. [Va88a, Va88b, Va91, Va92b]; for other research see e.g. survey [WoG93], PhD thesis [God96], papers [Pel93, GK+94], to mention only some). These methods take advantage of the fact that the total effect of a sequence of concurrent actions is independent of the order in which they are executed. (By the way, the term "partial-order" is misleading in this context and has always been disfavoured by us, but it is in common use because of historical reasons.)

Since 1988, several variations of the stubborn set method have been developed for many different verification tasks. The group has made a powerful test implementation [95-4] of a version of the stubborn set method suitable for process-algebraic verification with the CFFD semantics [Va92a]. The paper [Va92a] also shows how the CSP semantics can be handled. These results were extended in [96-7] to cover two more semantic models. First results on the use of stubborn sets with "high-level" specification formalisms where several identical processes can be defined with a single description were given in [98-2]. The key problem in that area is to avoid the "unfolding" of a process description to the corresponding set of process instances. A similar problem arises when data is represented in a symbolic form, and it was solved in [98-3].

Also the problem of detecting errors during the construction of the state space (on-the-fly verification) when stubborn sets are used has been investigated [93-3]. The size of the state space obtained with stubborn sets depends on both the system and the property that is being checked. In [97-4] it was shown how to avoid some state explosion that is due to the property during on-the-fly partial-order verification. Other advances towards an ideal combination of stubborn sets and on-the-fly methods were made in [00-2], which presented optimised methods for some commonly occurring specialised verification tasks.

The state of the art of stubborn sets and other partial-order methods was surveyed in [94-1]. Although it is now out of date, it may still be useful as a starting point because it is short and readable. The recommended first source on stubborn-set-type methods is now [98-4]. It contains a survey that is much more detailed, extensive and up-to-date than [94-1].

In addition to the results on combining on-the-fly verification with stubborn sets, the group has also investigated the construction of the tester automata used in process-algebraic on-the-fly verification, and adapted it to the CFFD semantics [00-1].

Compositional state space generation is another powerful technique for attacking the state explosion problem. Its basic idea is to reduce components of a system with respect to some equivalence notion before composing them together into the whole.

The group has analysed the prerequisites of compositional state space generation [93-2], expanded its scope from synchronous systems to shared-variable systems [94-2], and analysed the state explosion problem in the context of compositional analysis [95-2]. In co-operation with the University of Helsinki, the group has investigated several equivalence notions suitable for compositional analysis (see "Process-Algebraic Semantic Models" above).

In our earlier work we demonstrated that compositional analysis sometimes facilitates the verification of an infinite family of systems with a finite (and reasonable) amount of work [VaT91]. (A beautiful advanced application of this idea can be found in [Kai97], extracted from Roope Kaivola's PhD thesis [Kai96].) This idea was developed much further in [98-1], where integer parameters with unknown values were handled with compositionality. As an interesting application, the technique allowed the taking of so-called fairness assumptions into account, as was mentioned above. The paper won the "best paper award" of the conference where it was presented. Yet another example, namely a demand-driven token ring, is discussed in detail in [00-4].

A somewhat technical introduction to compositional state space generation covering also semantic models and algorithms was given in [96-4]. Also [98-4] and [00-4] contain lots of tutorial-type material on compositional state space generation.

Automated Testing of Concurrent Systems

In 1998 the group extended its activities to automatic testing of reactive systems. The first result in this field was the M.Sc. Thesis [99-2] that contains a survey on the part of testing theory that is based on process-algebraic concurrency theory. The group has adapted and extended one aspect of this theory, the canonical testers, to its favourite semantics in [00-1].

Tools

To test the practicality of its ideas and to facilitate research in verification methodology, the group has continued the tool development started by VTT Electronics (see 2. History and 4. ARA Toolset). The first version of ARA was described in [KL+92] and [93-1].

ARA was later expanded by two new state space generator tools. One of them allows the use of (limited) data types in its input language [95-3]. The other has a very weak input language but contains a powerful implementation of the stubborn set method [95-4]. Both tools facilitate compositional state space generation.

Building good tools requires also contributions to the theory. The paper [97-1] introduces a parallel composition operator of a new kind. It is much more flexible than the conventional ones from the modelling point of view, but still easily handled by verification tools. This operator can be used in an "intermediate language", to which high-level language specifications may be compiled for process-algebraic verification.

In 1999 the group started a major effort for building a new generation toolset that will replace ARA and its supplements. Many recent results by the group and by others have been taken into account in the design of the new toolset.

4. ARA Toolset

ARA is a collection of tools for finding errors in specifications and design models of concurrent and reactive systems. Examples of typical applications of ARA are deadlock detection in a mutual exclusion algorithm, and the checking whether a communication protocol conforms to its service specification.

ARA was originally developed by the Electronics research institute of the Technical Research Centre of Finland (VTT Electronics) (link in 7. Research Co-Operation). Some new parts of ARA have been developed by Tampere University of Technology. Many aspects of the background theory underlying ARA (including CFFD-equivalence) have been invented by the developers of ARA.

Input Language of ARA

The input language of ARA is Lotos with some modifications. Some information about Lotos was given already in 1. Introduction, and much more can be found from 8. Links to Relevant Topics. ARA Lotos was discussed in detail in [95-3].

The main difference between ARA Lotos and standard Lotos is that the data type system of ARA Lotos is modest. On the other hand, ARA Lotos contains extra features supporting error detection and verification. One of them makes it possible to present component processes of a system to ARA directly as labelled transition systems instead of Lotos expressions. This facilitates compositional LTS construction, the usefulness of which is described in 3. Research Themes and Results and also further down this section. The "illegal state" markers $error and $catastrophe are another verification-oriented feature worth mentioning here.

A complete ARA Lotos specification of a small system can be found in [96-1] (available also in HTML form).

Three Tools

The first stage of ARA, the ARA State Space Generator, transforms a Lotos description into a labelled transition system (LTS). An LTS is essentially a finite state machine representation of the behaviour of the system (see 1. Introduction).

Usually the next stage in the use of ARA is LTS reduction. ARA contains a tool called Normaliser which takes an LTS and produces a behaviourally equivalent, but typically much smaller LTS. The tool is called "Normaliser" instead of "Reducer" because it produces the same (except the naming of states) output LTS from all behaviourally equivalent input LTSs.

With ARA Comparator one can check whether two normalised LTSs are behaviourally equivalent. One can, for instance, use ARA to construct a normalised LTS from a protocol description and another normalised LTS from its service specification, and compare the two. The result of the comparison reveals whether the service provided by the protocol is the same as what was described in the service specification. If the behaviours are not equivalent, ARA Comparator provides an example of an execution which one but not the other of the two normalised LTSs may perform.

Points of View

One essential aspect in the use of ARA is the selection of a suitable point of view to the system under analysis. This is done by specifying what actions of the system are significant and what may be considered as implementation details.

For instance, when verifying that a communication protocol provides the correct service, actions in the user interface are important, and actions modelling the transmission of data messages and acknowledgements in the low-level communication channels are implementation details. For deadlock detection one may specify that all actions are implementation details. To verify mutual exclusion, entrance to and exit from the critical section are important.

In practice, actions are specified as implementation details by making them invisible in the Lotos description with the Lotos hide operator. Actions which are not invisible are visible.

ARA Illustrator

ARA Illustrator is a tool which shows small LTSs on computer screen in a graphical form. Normalised LTSs are often small enough for this purpose, in particular if the selected point of view is narrow enough. Deadlocks, violation of mutual exclusion and many other kinds of errors can be easily spotted from visualised LTSs.

It is difficult to find room for names of transitions in a visualisation of an LTS. Therefore, ARA Illustrator uses different colours to denote names. Below is an example of a visualised LTS produced by ARA Illustrator - we regret that it requires a colour screen to show out properly. The picture has been slightly edited by moving the name-colour map closer to the graph and by cutting away the empty space surrounding the graph.

A visualised LTS

Semantic Models in ARA

From the above it is obvious that the notion of behaviourally equivalent is essential in ARA. It determines what kinds of properties can be analysed and verified.

From among the vast collection of behavioural equivalence notions presented in the literature, the so-called Chaos-Free Failures Divergences Equivalence (CFFD-equivalence) [VaT91], [95-5] was chosen for ARA. It resembles the well-known failures/divergences equivalence of CSP theory [BrR85, Hoa85], [Ros98], but is in some respects more suited for verification.

The choice of an equivalence is a compromise between expressibility and efficiency. There are theoretical results demonstrating that CFFD-equivalence is an optimal choice for a natural and widely used class of verification questions, see 3. Research Themes and Results, subsection Process-Algebraic Semantic Models.

ARA and the State Explosion Problem

Like all verification tools, ARA is affected by the state explosion problem: LTSs of nontrivial systems tend to contain huge numbers of states. This problem is fundamental. It is extremely unlikely that it can be given a complete (or perhaps even satisfactory) solution in the foreseeable future, no matter what principles a verification tool is based on.

Many details of ARA have been designed with the state explosion problem in mind. In particular, a user of ARA can alleviate the problem by constructing LTSs compositionally, that is, by constructing and reducing LTSs for subsystems before combining them into the full system. A new version of the state space generator allows the use of other techniques such as stubborn sets (see 3. Research Themes and Results, in particular the Verification Methodology and Verification Case Studies, Techniques for Alleviating the State Explosion Problem and Tools subsections).

Users of ARA Known to Us

ARA has been used for both teaching and research purposes in the University of Helsinki and Tampere University of Technology. Kimmo Varpaaniemi of Helsinki University of Technology has implemented a link between its Prod Petri net verification tool and ARA.

Getting A Demo Version of ARA Tools by Anonymous FTP

VTT Electronics has made a demo version of the ARA toolset publicly available as described below. If there are problems with it, please inform Valmari (email link at end of page).


Availability of ARA Tools/Demo

ARA Tools/Demo is available from two anonymous ftp-machines:

nic.funet.fi
Sun SparcStation (Sun OS) version:
/pub/languages/lotos/ara201_Sparc.gzip
garbo.uwasa.fi
MS DOS, MS DOS 16 and MS Windows versions:
/pc/demo/ara201d.zip

Documentation (including User's Manual and Reference Manual) is included.

Distribution limitations

The use of ARA Tools/Demo is allowed only for non-profit research use, and for getting familiar with ARA Tools before making the decision of obtaining a licence for the full version. If you are interested to use ARA Tools for other purposes, please contact VTT Electronics for licence agreement (link in 7. Research Co-Operation).


5. Members

Head of the group

Antti Valmari Professor, Dr. Tech.

Postgraduate students

Undergraduate students

6. Funding

The majority of the funding of the group has come from

7. Research Co-Operation

The group is in close co-operation (joint publications) with

We have good contacts and occasional co-operation with

The group was involved in the European Union ESPRIT III Basic Research project #6021 REACT: Building Correct Reactive Systems. Links to it:

8. Links to Relevant Topics

Homepages of Individual Topics

More General Electronic Archives

Journals and Publishers Online

Others...

Please inform Valmari (email link at end of page).

9. Publications by the Group 1993-

The publications section has been moved into a file of its own: http://www.cs.tut.fi/ohj/VARG/publications/.

10. Other References

[BaK88] Back, R. J. R. & Kurki-Suonio, R.: Distributed Cooperation with Action Systems. ACM Transactions on Programming Languages and Systems, 10 (4) pp. 513-554, Oct. 1988.

[BoB87] Bolognesi, T. & Brinksma, E.: Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems 14 1987 pp. 25-59.

[BHR84] Brookes, S. D., Hoare, C. A. R. & Roscoe, A. W.: A Theory of Communicating Sequential Processes. Journal of the ACM, 31 (3) 1984, pp. 560-599.

[BrR85] Brookes, S. D. & Roscoe, A. W.: An Improved Failures Model for Communicating Sequential Processes. Proc. NSF-SERC Seminar on Concurrency, Lecture Notes in Computer Science 197, Springer-Verlag 1985, pp. 281-305.

[Eme90] Emerson, E. A.: Temporal and Modal Logic. Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, Elsevier Science Publishers 1990, pp. 995-1072.

[GK+94] Gerth, R., Kuiper, R., Peled, D. & Penczek, W.: A Partial Order Approach to Branching Time Logic Model Checking. Proceedings of the Third Israel Symposium on the Theory of Computing and Systems, IEEE 1995, pp. 130-139.

[God96] Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems, An Approach to the State-Explosion Problem. Lecture Notes in Computer Science 1032, Springer-Verlag 1996, 143 p. (Earlier version: PhD Thesis, University of Liège, 1994.)

[Hoa85] Hoare, C. A. R.: Communicating Sequential Processes. Prentice-Hall 1985, 256 p.

[ISO89] ISO 8807 International Standard: Information processing systems - Open Systems Interconnection - LOTOS - A formal description technique based on the temporal ordering of observational behaviour. International Organization for Standardization 1989, 142 p.

[Jen92] Jensen, K.: Coloured Petri Nets, Vol. 1: Basic Concepts. EATCS Monographs on Theoretical Computer Science, Springer-Verlag 1992, 234 p.

[Kai96] Kaivola, R.: Equivalences, Preorders and Compositional Verification for Linear Time Temporal Logic and Concurrent Systems. PhD Thesis, University of Helsinki, Department of Computer Science, Report A-1996-1, Helsinki, Finland 1996, 185 p.

[Kai97] Kaivola, R.: Using Compositional Preorders in the Verification of Sliding Window Protocol. Computer Aided Verification, 9th International Conference, CAV'97, Haifa, Israel, June 1997, Proceedings, Lecture Notes in Computer Science 1254, Springer-Verlag 1997, pp. 48-59.

[KaV92] Kaivola, R. & Valmari, A.: The Weakest Compositional Semantic Equivalence Preserving Nexttime-less Linear Temporal Logic. Proceedings of CONCUR '92, Lecture Notes in Computer Science 630, Springer-Verlag 1992, pp. 207-221.

[KL+92] Kemppainen, J., Levanto, M., Valmari, A. & Clegg, M.: "ARA" Puts Advanced Reachability Analysis Methods Together. Proceedings of the Fifth Nordic Workshop on Programming Environment Research, Tampere, Finland, January 1992, Tampere University of Technology, Software Systems Laboratory, Report 14. An earlier version of [93-1].

[KJ+90] Kurki-Suonio, R., Järvinen, H.-M., Sakkinen, M. & Systä, K.: Object-oriented Specification of Reactive Systems. Proceedings of the 12th International Conference on Software Engineering, pp. 63-71, IEEE Computer Society Press, 1990.

[MaP92] Manna, Z. & Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag 1992, 427 p.

[Mil89] Milner, R.: Communication and Concurrency. Prentice-Hall 1989, 260 p.

[Mur89] Murata, T.: Petri Nets: Properties, Analysis and Applications. Proceedings of the IEEE 77 (4) 1989 pp. 541-580.

[Pel93] Peled, D.: All from One, One for All: On Model Checking Using Representatives. Proceedings of CAV '93, 5th International Conference on Computer-Aided Verification, Elounda, Greece, Lecture Notes in Computer Science 697, Springer-Verlag 1993, pp. 409-423.

[Ros94] Roscoe, A. W.: Model-Checking CSP. A Classical Mind: Essays in Honour of C. A. R. Hoare, Prentice-Hall 1994, pp. 353-378.

[Ros98] Roscoe, A. W.: The Theory and Practice of Concurrency. Prentice-Hall 1998, 565 p.

[Va88a] Valmari, A.: Error Detection by Reduced Reachability Graph Generation. Proceedings of the 9th European Workshop on Application and Theory of Petri Nets, Venice, Italy 1988, pp. 95-112.

[Va88b] Valmari, A.: State Space Generation: Efficiency and Practicality. PhD Thesis, Tampere University of Technology Publications 55, 1988, 169 p.

[Val91] Valmari, A.: Stubborn Sets for Reduced State Space Generation. Advances in Petri Nets 1990, Lecture Notes in Computer Science 483, Springer-Verlag 1991, pp. 491-515. (Earlier version: Proceedings of the 10th International Conference on Application and Theory of Petri Nets, Bonn, West Germany 1989, Vol II, pp. 122.)

[Va92a] Valmari, A.: Alleviating State Explosion during Verification of Behavioural Equivalence. Department of Computer Science, University of Helsinki, Report A-1992-4, Helsinki, Finland 1992, 57 p.

[Va92b] Valmari, A.: A Stubborn Attack on State Explosion. Formal Methods in System Design, 1: 297-322 (1992). (Earlier version: 2nd International Conference on Computer-Aided Verification, New Brunswick, NJ, USA 1990.)

[VaT91] Valmari, A. & Tienari, M.: An Improved Failures Equivalence for Finite-State Systems with a Reduction Algorithm. Protocol Specification, Testing and Verification XI (Proceedings of 11th International IFIP WG 6.1 Symposium on Protocol Specification, Testing and Verification, Stockholm, Sweden, June 1991), North-Holland 1991, pp. 3-18.

[Wol93] Wolper, P.: Esprit Basic Research Action REACT (6021): Building Correct Reactive Systems. EATCS Bulletin 50, June 1993, pp. 138-153.

[WoG93] Wolper, P. & Godefroid, P: Partial-Order Methods for Temporal Verification. Proceedings of CONCUR '93, Lecture Notes in Computer Science 715, Springer-Verlag 1993, pp. 233-246.


Antti Valmari, ava@cs.tut.fi