DisCo swMATH ID: 10393 Software Authors: Aaltonen, Timo; Katara, Mika; Pitkänen, Risto Description: DisCo Toolset – the new generation. Formal methods have been considered one possible solution to the so-called software crisis. Tools are valuable companions to formal methods: they assist in analysis and understanding of formal specifications and enable the use of rigorous techniques in industrial projects. In this paper, an overview of the new DisCo toolset is given. DisCo is a formal specification method for reactive and distributed systems. It focuses on collective behaviour of objects and provides a refinement mechanism that preserves safety properties. The toolset currently includes a compiler, a graphical animation tool, and a scenario tool for representing execution traces as message sequence charts. A prototype verification back-end based on the PVS theorem prover also exists, and a model checking back-end based on Kronos as well as code generation facilities have been planned. In this paper, the operation of the DisCo toolset is illustrated by applying it to an example specification describing a simple cash-point service system. Homepage: http://jucs.org/jucs_7_1/disco_toolset_the_new/Aaltonen_T.pdf Keywords: DisCo toolset Related Software: PVS; AspectJ; Ocsid; HOL-UNITY; HOL; Coq; Kronos Cited in: 7 Publications all top 5 Cited by 8 Authors 3 Aaltonen, Timo 2 Katara, Mika 2 Kellomäki, Pertti 2 Mikkonen, Tommi 1 Franch, Xavier 1 Kurki-Suonio, Reino 1 Marco, Jordi 1 Pitkänen, Risto Cited in 2 Serials 1 Annales Universitatis Scientiarum Budapestinensis de Rolando Eötvös Nominatae. Sectio Computatorica 1 Journal of Universal Computer Science Cited in 1 Field 7 Computer science (68-XX) Citations by Year