To make this possible, a theory of programs should provide a comprehensive set of abstractions, where
The ideas have evolved in project DisCo, in connection with developing an experimental specification and modeling language with the same name. The underlying philosophy has led to a linear-time state-based approach, with TLA (temporal logic of actions) as its logical foundation. The closed-system principle of modeling a system always together with its assumed environment leads to intuitively natural reasoning about collective behaviors. The execution model of operational specifications in this approach is based on multi-object actions, and has a close relationship to the logic used for reasoning.
Perhaps the most important aspect of the approach is the incremental design methodology that is supported. Its theoretical basis is in superposition-based refinement, where the preservation of safety properties is guaranteed by construction. The inherent restrictions of superposition are overcome by the possibility to eliminate variables that have become redundant "ghost variables" in the design process. A proof methodology is introduced for preservation of liveness properties and for elimination of redundant variables.
In my opinion, a practical specification formalism has to be operational. It needs concepts that are familiar from programming languages, but conceptually it has to be much simpler, and it also requires a formal basis for rigorous reasoning. I find that most approaches to object-oriented specification of reactive systems are either too theoretical or are burdened by implementation-oriented complexities taken from programming languages. Of course, it is difficult to find proper abstractions that allow simplicity without being too simple. This is, however, what I have tried to do.
After many years of (re)writing, a manuscript for a book on this topic is now (Feb 2004) available, and I hope to get it published in the near future.
R. Kurki-Suonio, Action systems in incremental and aspect-oriented modeling. Distributed Computing 16, 201-217, 2003.
R. Kurki-Suonio, Component and interface refinement in closed-system specifications. Manuscript 1999 (compressed postscript)
R. Kurki-Suonio, M. Katara, Logical Layers in Specifications with Distributed
Objects and Real Time. To appear in IJSSE.
Discusses how real time is supported in the approach, and how derivation by
superposition and composition allows to separate different aspects of a
specification into different layers. Periodic and aperiodic events are
described in terms of abstract classes. (An extended and revised version of
a paper that appeared in Proc. 1st IEEE International Symposium on
Object-Oriented Real-Time Distributed Systems, ISORC'98, IEEE Computer Society.
Compressed postscript of an earlier version.)
R. Kurki-Suonio, T. Mikkonen, Abstractions of distributed cooperation, their refinement and implementation. Proc. International Symposium on Software for Parallel and Distributed Systems, PDSE'98 (eds. Bernd Krämer, Naoshi Uchihira, Peter Croll, Stefano Russo), IEEE Computer Society 1998, 94-102.
R. Kurki-Suonio, T. Mikkonen,
Harnessing the power of interaction. Invited paper in Proc.
8th European-Japanese Conference on Information Modelling and Knowledge Bases.
In Information Modelling and Knowledge Bases X (Eds. H. Jaakkola,
H. Kangassalo, E. Kawaguchi), IOS Press 1999, 1-11.
(Compressed postscript)
A "position paper" that analyzes at a very general level why the specification
of interactive systems needs to be based on the paradigm of reactive systems,
not on the traditional algortihmic paradigm, as is usually done.
R. Kurki-Suonio, T. Mikkonen, Liberating object-oriented modeling from
programming-level
abstractions. In Object-Oriented Technology (Eds. J. Bosch, S. Mitchell),
LNCS 1357, Springer-Verlag 1998, 195-199.
Discusses how the complexities of object-oriented programming can and should
be avoided at the level of specifications.
(Compressed postscript of an earlier
version given at an ECOOP'97 Workshop)
R. Kurki-Suonio, Incremental specification with joint actions: the RPC-memory
specification problem. In Formal Systems Specification (Eds. M. Broy, S. Merz, K. Spies), LNCS 1169, Springer- Verlag 1996, 375-404. (Postscript available on request.)
Uses the approach to derive a solution to a specification problem. The volume
contains various solutions using different specification techniques.
R. Kurki-Suonio, Fundamentals of object-oriented specification and modeling of
collective behaviors. In Object-Oriented Behavioral Specifications (Eds. H. Kilov, W.
Harvey), Kluwer Academic Publishers 1996, 101-120. (Postscript available on request.)
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.
R. Kurki-Suonio, Real time: further misconceptions or half-truths. IEEE Computer
27, 6, June 1994, 71-76.
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.
R. Kurki-Suonio, Hybrid models with fairness and distributed clocks. In Hybrid
Systems (Eds. R.L. Grossman et al.), LNCS 736, Springer-Verlag 1993, 103-120.
Analyzes how the approach can be used for real-time and hybrid systems.
R. Kurki-Suonio, K. Systä, J. Vain, Real-time specification and modeling with
joint actions. Science of Computer Programming 20, April 1993, 113-140.
Based on a workshop paper, where real-time specification with this approach was
first discussed.
R. Kurki-Suonio, Stepwise design of real-time systems. IEEE Trans. on Software
Engineering 19, 1, Jan. 1993, 56-69.
Based on a SIGSOFT conference paper, where the design methodology of the approach was
considered for real-time systems.
N. Francez, R.J.R. Back, R. Kurki-Suonio, On equivalence-completions of fairness
assumptions. Formal Aspects of Computing 4, 6, 1992, 582-591.
Analyzes such fairness notions in distributed systems that are not equivalence robust.
Further development of ideas presented in an ICALP paper mentioned below.
R. Kurki-Suonio, Modular modeling of temporal behaviors. In Information Modelling
and Knowledge Bases III (Eds. S Ohsuga et al.), IOS Press, 1992, 283-300.
Demonstrates incremental modeling using the "doctors' office" example.
K. Systä, R. Kurki-Suonio, Modeling of distributed real-time systems in DisCo. Proc. Fourth
Euromicro Workshop on Real-Time Systems, Athens, Greece, June 1992, IEEE
Computer Society Press, 136-141.
Discusses real-time modeling with the approach, with an emphasis on using the
DisCo tool.
Postscript available.
R. Kurki-Suonio, Operational specification with joint actions: serializable
databases. Distributed Computing 6, 1, January 1992, 19-37.
Demonstrates incremental modeling with the approach.
R. Kurki-Suonio, K. Systä, J. Vain, Scheduling in real-time models. Formal
Techniques in Real-Time and Fault Tolerant Systems (Ed. J. Vytopil), LNCS 571,
Springer-Verlag, 1991, 327-339.
Discusses real-time modeling with the approach.
Postscript available.
H.-M. Järvinen, R. Kurki-Suonio, DisCo specification language: marriage of
actions and
objects. Proc. 11th International Conference on Distributed Computing Systems, IEEE
Computer Society Press, 142-151, 1991.
Discusses the DisCo language and design methodology in the light of the alternating
bit protocol example.
Postscript available.
R. Kurki-Suonio, Towards languages that support program derivation, or control
modularity considered harmful. Acta Cybernetica 9, 179-192, 1990.
Argues against using conventional control-based modularity in specification and
design languages.
H.-M. Järvinen, R. Kurki-Suonio, M. Sakkinen, K. Systä, Object-oriented
specification of
reactive systems. Proc. 12th International Conference on Software Engineering, IEEE
Computer Society Press, 63-71, 1990.
Supercedes the following.
Postscript available.
R. Kurki-Suonio, H.-M. Järvinen, Action system approach to the specification and
design of distributed systems. Proc. 5th International Workshop on Software
Specification and Design, ACM Software Engineering Notes 14, 34-40, 1989.
The ideas of DisCo were first published here.
R.J.R. Back, R. Kurki-Suonio, Decentralization of process nets with a centralized
control. Distributed Computing 3, 73-87, 1989. 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.J.R. Back, R. Kurki-Suonio, Distributed cooperation with action systems. ACM
Transactions on Programming Languages and Systems 10, 513-554, 1988.
A basic paper about joint action systems.
R.J.R. Back, R. Kurki-Suonio, Serializability in distributed systems with handshaking.
Proc. ICALP 88, LNCS 317, Springer-Verlag, 52-66, 1988.
Analyzes the different fairness notions that are natural for action systems.
R. Kurki-Suonio, T. Kankaanpää, On the design of reactive systems. BIT 28,
581-604, 1988.
The specification of a simplified telephone exchange is discussed. Was written when
the ideas of DisCo were still in early stages of development.
R. Kurki-Suonio, Towards programming with knowledge expressions. Proc. ACM
Conference on Principles of Programming Languages 86, ACM, 140-149, 1986.
Discusses development of distributed programs in terms of knowledge logic.
Uses joint actions and the same example as the "Decentralization of process nets ..."
paper.