The DisCo Home Page

Publications of the DisCo group with annotations

Click here for BibTeX data

1. Papers

2. Theses

3. Technical Reports

4. Others

1. Papers

Pertti Kellomäki. Composing Distributed Systems from Reusable Aspects of Behavior. In Proceedings of ICDCS'02 Workshops. IEEE Press, 2002.

Tommi Mikkonen and Risto Pitkänen. Facilities of Practice Reflecting Abstractions of Theory, and Vice Versa. In Proceedings of the XXI International Conference of the Chilean Computer Science Society, SCCC 2001, pages 203-212. IEEE Computer Society, 2001.

Pertti Kellomäki. A Structural Embedding of Ocsid in PVS. In Richard J. Boulton and Paul B. Jackson, editors, Theorem Proving in Higher Order Logics, TPHOLS2001, number 2152 in Lecture Notes in Computer Science, pages 281-296. Springer Verlag, 2001.

Mika Katara and Tommi Mikkonen. Aspect-Oriented Specification Architectures for Distributed Real-Time Systems. In Sten F. Andler, Michael G. Hinchey, and Jeff Offutt, editors, Proceedings of the Seventh IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2001, pages 180-190, Skövde, Sweden, June 2001. IEEE Computer Society Press.

Pertti Kellomäki. Deriving Message Passing Protocols From Collective Behavior. In Bernd Kleinjohann, editor, Architecture and Design of Distributed Embedded Systems, proceedings of the IFIP WG10.3/WG10.4/WG10.5 International Workshop on Distributed and Parallel Embedded Systems (DIPES 2000), pages 183-192. Kluwer Academic Publishers, 2001.

Mika Katara and Arto Luoma. Environment Modelling in Closed Specifications of Embedded Systems. In Bernd Kleinjohann, editor, Architecture and Design of Distributed Embedded Systems, proceedings of the IFIP WG10.3/WG10.4/WG10.5 International Workshop on Distributed and Parallel Embedded Systems (DIPES 2000), pages 141-150. Kluwer Academic Publishers, 2001.

Timo Aaltonen, Mika Katara, and Risto Pitkänen. DisCo Toolset - The New Generation. Journal of Universal Computer Science, 7(1):3-18, 2001.

Timo Aaltonen, Pertti Kellomäki, and Risto Pitkänen. Specifying Cash-Point with DisCo. Formal Aspects of Computing, 12(4):231-232, 2000.

Mika Katara. Hybrid Models for Mobile Computing. In António Porto and Gruia-Catalin Roman, editors, Coordination Languages and Models, 4th International Conference, COORDINATION 2000, Proceedings, number 1906 in Lecture Notes in Computer Science, pages 216-231. Springer-Verlag, 2000.

Reino Kurki-Suonio and Tommi Mikkonen. From Program Construction to Abstraction Engineering. In Yulin Feng, David Notkin, and Marie-Claude Gaudel, editors, 16th World Computer Congress 2000, Proceedings of Conference on Software: Theory and Practice, pages 861-868, Beijing, China, August 2000. Publishing House of Electronics Industry and International Federation for Information Processing. IFIP.

Pertti Kellomäki. Verification-Friendly Specification of Distributed Systems. In Yulin Feng, David Notkin, and Marie-Claude Gaudel, editors, 16th World Computer Congress 2000, Proceedings of Conference on Software: Theory and Practice, pages 480-483, Beijing, China, August 2000. Publishing House of Electronics Industry and International Federation for Information Processing. IFIP.

Timo Aaltonen, Mika Katara, and Risto Pitkänen. Verifying Real-Time Joint Action Specifications Using Timed Automata. In Yulin Feng, David Notkin, and Marie-Claude Gaudel, editors, 16th World Computer Congress 2000, Proceedings of Conference on Software: Theory and Practice, pages 516-525, Beijing, China, August 2000. Publishing House of Electronics Industry and International Federation for Information Processing. IFIP.

Pertti Kellomäki and Tommi Mikkonen. Design Templates for Collective Behavior. In Elisa Bertino, editor, Proceedings of ECOOP 2000, 14th European Conference on Object-Oriented Programming, number 1850 in Lecture Notes in Computer Science, pages 277-295. Springer-Verlag, 2000.

Mika Katara and Tommi Mikkonen. Design Approach for Real-Time Reactive Systems. In P.-A. Hsiung and F. Wang, editors, Proceedings of the International Workshop on Real-Time Constraints, pages 11-20, Alexandria, Virginia, USA, October 1999.

Reino Kurki-Suonio. Component and Interface Refinement in Closed-System Specifications. In J. Wing, J. Woodcock, and J. Davies, editors, FM'99 - Formal Methods: World Congress on Formal Methods in the Development of Computing Systems, number 1708 in Lecture Notes in Computer Science, pages 134-154. Springer-Verlag, 1999.

Pertti Kellomäki and Tommi Mikkonen. Archived Design Steps in Temporal Logic. In J. Wing, J. Woodcock, and J. Davies, editors, FM'99 - Formal Methods: World Congress on Formal Methods in the Development of Computing Systems, number 1708 in Lecture Notes in Computer Science, pages 1858-1858. Springer-Verlag, 1708.

Mika Katara. Composing DisCo Specifications Using Generic Real-Time Events - A Mobile Robot Case Study. In Jaan Penjam, editor, Software Technology, Proceedings of the Fenno-Ugric Symposium FUSST'99, pages 75-86, Sagadi, Estonia, August 1999. Institute of Cybernetics at Tallinn Technical University (Technical Report CS 104/99).

Reino Kurki-Suonio and Mika Katara. Logical layers in specifications with distributed objects and real time. Computer Systems Science & Engineering, 14(4):217-226, July 1999.

Risto Pitkänen and Harri Klapuri. Incremental Cospecification Using Objects and Joint Actions. In H. R. Arabnia, editor, Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'99), pages 2961-2967. CSREA Press, June 1999.

Tommi Mikkonen. Codesign Requires Closed-System Specifications. In H. R. Arabnia, editor, Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'99), pages 2968-2974. CSREA Press, June 1999.

Reino Kurki-Suonio and Tommi Mikkonen. Harnessing the power of interaction. In H. Jaakkola, H. Kangassalo, and E. Kawaguchi, editors, Information Modelling and Knowledge Bases X, pages 1-11. IOS Press, 1999.

Pertti Kellomäki and Tommi Mikkonen. Modeling Distributed State as an Abstract Object. In Distributed and Parallel Embedded Systems, proceedings of the IFIP WG 10.3 / WG 10.5 International Workshop on Distributed and Parallel Embedded Systems (DIPES'98), pages 223-230. Kluwer Academic Publishers, 1999.

Reino Kurki-Suonio and Tommi Mikkonen. Harnessing the Power of Interaction. In H. Jaakkola and H. Kangassalo, editors, Proceedings of the 8th European-Japanese Conference on Information Modelling and Knowledge Bases, number A 19 in Series A - Pori School of Technology and Economics, pages 1-14, May 1998.

Tommi Mikkonen. Formalizing Design Patterns. In B. Werner, editor, Proceedings of the 20th International Conference on Software Engineering (ICSE'98), pages 115-124. IEEE Computer Society, April 1998.

Tommi Mikkonen and Hannu-Matti Järvinen. Specifying for Releases. In Proceedings of the International Workshop on Principles of Software Evolution IWPSE98, pages 118-122, April 1998.

Reino Kurki-Suonio and Tommi Mikkonen. Abstractions of Distributed Cooperation, their Refinement and Implementation. In B. Krämer, N. Uchihira, P. Croll, and S. Russo, editors, Proceedings of the International Symposium on Software Engineering for Parallel and Distributed Systems, pages 94-102. IEEE Computer Society, April 1998.

Reino Kurki-Suonio and Mika Katara. Real Time in a TLA-Based Theory of Reactive Systems. In Proceedings of the first IEEE International Symposium on Object-oriented Real-time distributed Computing, pages 186-195. IEEE Computer Society, April 1998.

Tommi Mikkonen. A Development Cycle for Dependable Reactive Systems. In Y. Chen, editor, Proceedings of the 1998 International IFIP Workshop on Dependable Computing and Its Applications, pages 70-82, Johannesburg, South Africa, 1998. University of Witwatersrand.

Reino Kurki-Suonio and Tommi Mikkonen. Liberating Object-Oriented Modeling from Programming-Level Abstractions. In J. Bosch and S. Mitchell, editors, Object-Oriented Technology, ECOOP'97 Workshop Reader, number 1357 in Lecture Notes in Computer Science, pages 195-199. Springer-Verlag, 1998.

Pertti Kellomäki. Verification of Reactive Systems Using DisCo and PVS. In John Fitzgerald, Cliff B. Jones, and Peter Lucas, editors, FME'97: Industrial Applications and Strengthened Foundations of Formal Methods, number 1313 in Lecture Notes in Computer Science, pages 589-604. Springer-Verlag, 1997.

Annotation: Describes verification of reactive systems using the alternating bit protocol as an example. Translation from DisCo to the logic of the PVS theorem prover is illustrated using the example.

Pertti Kellomäki. Using Auxiliary Knowledge in Automating Invariant Proofs. In Joakim von Wright, Jim Grundy, and John Harrison, editors, Supplementary Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics: TPHOLs'96, pages 57-68. Turku Centre for Computer Science, August 1996.

Annotation: Describes how invariant proofs of DisCo specifications are partly automated by generating strategies for the PVS theorem prover.

Pertti Kellomäki. Mechanical Verification of DisCo Specifications. In Israeli-Finnish Binational Symposium on Specification, Development, and Verification of Concurrent Systems, The Technion, Haifa, January 1996.

Annotation: Describes verification of DisCo invariants in a general level.

Reino Kurki-Suonio. Fundamentals of object-oriented specification and modeling of collective behaviors. In H. Kilov and W. Harvey, editors, Object-Oriented Behavioral Specifications , pages 101-120. Kluwer Academic Publishers, 1996.

Annotation: Provides a general introduction to the different components of the approach. Real-time modeling is also discussed briefly, and using an intuitively more natural technique than the earlier papers on real-time modeling.

Reino Kurki-Suonio. Incremental specification with joint actions: the RPC-memory specification problem. In M. Broy, S. Merz, and K. Spies, editors, Formal Systems Specification, number 1169 in Lecture Notes in Computer Science, pages 375-404. Springer-Verlag, 1996.

Annotation: Uses the joint action approach to derive a solution to a specification problem. The volume contains various solutions using different specification techniques.

Pertti Kellomäki. Mechanizing Invariant Proofs of Joint Action Systems. In Proceedings of the Fourth Symposium on Programming Languages and Software Tools, pages 141-152, Visegrad, Hungary, June 1995.

Annotation: Describes initial attempts for formalizing DisCo in the PVS theorem prover and proving invariants.

Tommi Mikkonen. An experimental code generator for implementing formal specifications given as closed systems. In Proceedings of the Fourth Symposium on Programming Languages and Software Tools, Visegrad, Hungary, June 1995.

Tommi Mikkonen. Partitioning DisCo specifications. In IEE Colloquium on Partitioning in hardware-software codesigns, London, United Kingdom, February 1995.

Pertti Kellomäki. Self Stabilization of a Protocol. In Proceedings of the Nordic Seminar on Dependable Computing Systems, Lyngby, Denmark, 24.-26. August 1994.

Annotation: A short version of Pertti's licentiate thesis. Gives an overview of the specification and verification of a distributed token ring protocol.

Reino Kurki-Suonio. Real time: further misconceptions or half-truths. IEEE Computer, 27(6):71-76, June 1994.

Annotation: Analyzes the notion of real time in specification models. Addresses, in particular, issues related to fairness and the direction of causality between time and events.

Kari Systä. Specifying User Interfaces in DisCo. ACM SIGCHI Bulletin, 26(2):53-58, April 1994.

Kari Systä. Specifying User Interfaces as Joint Action Systems. In Proceedings of the Third Symposium on Programming Languages and Software Tools, pages 130-141. University of Tartu, 1993.

Tommi Mikkonen. On implementing object-oriented specifications given as closed systems. In Conceptual Modeling and Object-Oriented Programming. Finnish Artificial Intelligence Society, November 1993.

Hannu-Matti Järvinen, Reino Kurki-Suonio, and Kari Systä. Experiences in object-oriented modeling with multi-object actions (invited lecture). In H. Kilov and B. Harvey, editors, Proceedings of the OOPSLA'93 Workshop on Specification of Behavioral Semantics in Object-Oriented Information Modeling, pages 61-66, Robert Morris College, 1993.

R. Kurki-Suonio, K. Systä, and J. Vain. Real-time specification and modeling with joint actions. Science of Computer Programming, (20):113-140, April 1993.

Annotation: Based on a workshop paper, where real-time specification with this approach was first discussed.

Reino Kurki-Suonio. Hybrid models with fairness and distributed clocks. In R.L. Grossman et al., editor, Hybrid Systems, number 736 in Lecture Notes in Computer Science, pages 103-120. Springer-Verlag, 1993.

Annotation: Analyzes how the approach can be used for real-time and hybrid systems.

Reino Kurki-Suonio. Stepwise Design of Real-Time Systems. IEEE Transactions on Software Engineering, 19(1):56-69, January 1993.

Annotation: Based on a SIGSOFT conference paper, where the design methodology of the approach was considered for real-time systems.

K. Systä and R. Kurki-Suonio. Modeling of distributed real-time systems in DisCo. In Proceedings of the Fourth Euromicro Workshop on Real-Time Systems, pages 136-141, Athens, Greece, June 1992. IEEE Computer Society Press.

Annotation: Discusses real-time modeling with the approach, with an emphasis on using the DisCo tool

Reino Kurki-Suonio. Operational specification with joint actions: serializable databases. Distributed Computing, 6(1):19-37, January 1992.

Annotation: Demonstrates incremental modeling with the approach.

Reino Kurki-Suonio. Modular modeling of temporal behaviors. In S. Ohsuga et al., editor, Information Modelling and Knowledge Bases III, pages 283-300. IOS Press, 1992.

Annotation: Demonstrates incremental modeling using the "doctors' office" example.

Nissim Francez, Ralph-J. J. Back, and Reino Kurki-Suonio. On Equivalence-completions of Fairness Assumptions. Formal Aspects of Computing, 6(4):582-591, 1992.

Annotation: Analyzes such fairness notions in distributed systems that are not equivalence robust. Further development of ideas presented in an ICALP paper in 1988.

R. Kurki-Suonio, K. Systä, and J. Vain. Scheduling in real-time models. In J. Vytopil, editor, Formal Techniques in Real-Time and Fault Tolerant Systems, number 571 in Lecture Notes in Computer Science, pages 327-339. Springer-Verlag, 1991.

Annotation: Discusses real-time modeling with the approach.

Kari Systä. A Graphical Tool for Specification of Reactive Systems. In Proceedings of the Euromicro'91 Workshop on Real-Time Systems, pages 12-19, Paris, France, June 1991. IEEE Computer Society Press.

Annotation: Describes the animation tool.

Hannu-Matti Järvinen and Reino Kurki-Suonio. DisCo specification language: marriage of actions and objects. In Proceedings of the 11th International Conference on Distributed Computing Systems, pages 142-151. IEEE Computer Society Press, 1991.

Annotation: Discusses the DisCo language and design methodology in the light of the alternating bit protocol example

H.-M. Järvinen, R. Kurki-Suonio, M. Sakkinen, and K. Systä. Object-oriented specification of reactive systems. In Proceedings of the 12th International Conference on Software Engineering, pages 63-71. IEEE Computer Society Press, 1990.

Annotation: Supersedes the workshop paper that appeared in Software Engineering Notes in 1989.

Reino Kurki-Suonio. Towards languages that support program derivation, or control modularity considered harmful. Acta Cybernetica, (9):179-192, 1990.

Annotation: Argues against using conventional control-based modularity in specification and design languages.

R. J. R. Back and R. Kurki-Suonio. Decentralization of process nets with centralized control. Distributed Computing, 3:73-87, 1989.

Annotation: An earlier version in Proc. ACM Conference on Principles of Distributed Conputing, ACM, 131-142, 1983. The notion of joint actions was first introduced in this 1983 conference paper. The ideas are developed in the paper by deriving a CSP solution to a simple distributed sorting problem.

R. Kurki-Suonio and H.-M. Järvinen. Action system approach to the specification and design of distributed systems. In Proceedings of the 5th International Workshop on Software Specification and Design, number 14 in ACM Software Engineering Notes, pages 34-40, 1989.

Annotation: The ideas of DisCo were first published here.

R. J. R. Back and R. Kurki-Suonio. Serializability in distributed systems with handshaking. In Proceedings of ICALP 88, number 317 in Lecture Notes in Computer Science, pages 52-66. Springer-Verlag, 1988.

Annotation: Analyzes the different fairness notions that are natural for action systems.

R. J. R. Back and R. Kurki-Suonio. Distributed cooperation with action systems. ACM Transactions on Programming Languages and Systems, 10(4):513-554, October 1988.

Annotation: A basic paper about joint action systems.

R. Kurki-Suonio and T. Kankaanpää. On the design of reactive systems. BIT, (28):581-604, 1988.

Annotation: The specification of a simplified telephone exchange is discussed. Was written when the ideas of DisCo were still in early stages of development.

Reino Kurki-Suonio. Towards programming with knowledge expressions. In Proceedings of the ACM Conference on Principles of Programming Languages, pages 140-149. ACM, 1986.

Annotation: Discusses development of distributed programs in terms of knowledge logic. Uses joint actions and the same example as the "Decentralization of process nets ..." paper.

2. Theses

Mika Katara. Aspects of Continuous Behaviour - Design of Real-Time Reactive Systems in DisCo. PhD thesis, Tampere University of Technology, 2001.

Tommi Mikkonen. Abstractions and Logical Layers in Specifications of Reactive Systems. PhD thesis, Tampere University of Technology, 1999.

Pertti Kellomäki. Mechanical Verification of Invariant Properties of DisCo Specifications. PhD thesis, Tampere University of Technology, 1997.

Annotation: The thesis describes how the DisCo language is mapped to the logic of the PVS theorem prover, and how the mapping is used for verification of invariants. The methodology used in verification is based on verifying invariants at a high level of abstraction, and then verifying that the lower levels correctly implement the abstractions.

Risto Pitkänen. DisCo-spesifikaatioiden simulointi Javalla (Simulation of DisCo Specifications in Java). Master's thesis, Tampere University of Technology, June 1997.

Mika Katara. Spesifikaatioiden strukturoinnista TLA+:ssa ja DisCossa (On structuring of specifications in TLA+ and DisCo). Master's thesis, Tampere University of Technology, September 1996.

Timo Aaltonen. DisCo-kielen kehittämisestä (On developing the DisCo language). Master's thesis, Tampere University of Technology, March 1996.

Kari Systä. A Specification Method for Interactive Systems. PhD thesis, Tampere University of Technology, 1995.

Tommi Mikkonen. Implementation of reactive systems based on closed-system specifications. Licentiate of Technology thesis, Tampere University of Technology, 1995.

Pertti Kellomäki. Analysis of a Stabilizing Protocol. Licentiate of Technology thesis, Tampere University of Technology, 1994.

Annotation: Gives a detailed DisCo specification of a distributed token ring protocol, and a hand verification of the stabilization properties of the protocol.

Tommi Mikkonen. Formaalin määrittelyn toteutusperiaatteet. Master's thesis, Tampere University of Technology, 1992.

Hannu-Matti Järvinen. The design of a specification language for reactive systems. PhD thesis, Tampere University of Technology, 1992.

Manu Setälä. Lentokoneen avioniikan formaali mallintaminen (Formal modeling of an avionics system). Master's thesis, Tampere University of Technology, 1992.

Tatu Männisto. DisCo-spesifiointikielen virtuaalikone (A virtual machine for the DisCo specification language). Master's thesis, Tampere University of Technology, 1992.

Kari Systä. Suoritettavien spesifikaatioiden visualisointi- ja animointijärjestelmä (Visualization and Animation of Executable Specifications). Licentiate of Technology thesis, Tampere University of Technology, 1990.

Olavi Eerola. Suoritettavan spesifiointikielen kääntäjä (A Compiler for an Executable Specification Language). Master's thesis, Tampere University of Technology, 1990.

3. Technical Reports

Timo Aaltonen and Risto Pitkänen. Verifying Safety by Combining Joint Actions with a Process-Algebraic Approach. Technical Report 19, Tampere University of Technology, Software Systems Laboratory, 1999.

Tommi Mikkonen. A Layer-Based Formalization of an On-Board Instrument. Technical Report 18, Tampere University of Technology, Software Systems Laboratory, 1998.

Hannu-Matti Järvinen and Reino Kurki-Suonio. The DisCo Language and Temporal Logic of Actions. Technical Report 11, Tampere University of Technology, Software Systems Laboratory, 1990.

Hannu-Matti Järvinen and Reino Kurki-Suonio. The DisCo Language. Technical Report 8, Tampere University of Technology, Software Systems Laboratory, 1990.

4. Others

The DisCo Tutorial. At URL http://disco.cs.tut.fi on the World Wide Web.

The DisCo project WWW page. At \urlhttp://disco.cs.tut.fi on the World Wide Web.