@InProceedings{pk:aopdcs02,
  author = 	 {Pertti Kellom{\"a}ki},
  title = 	 {Composing Distributed Systems from Reusable Aspects of Behavior},
  booktitle = 	 {Proceedings of ICDCS'02 Workshops},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTpages = 	 {},
  year =	 {2002},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  publisher =	 {IEEE Press},
  note =	 {To appear},
  OPTannote = 	 {}
}

@InProceedings{tjm+:sccc01,
  author = 	 {Tommi Mikkonen and Risto Pitk{\"a}nen},
  title = 	 {Facilities of Practice Reflecting Abstractions
                  of Theory, and Vice Versa},
  booktitle = 	 {Proceedings of the XXI International Conference of the Chilean
                  Computer Science Society, SCCC 2001},
  pages =	 {203--212},
  publisher =	 {IEEE Computer Society},
  year =	 2001,
  month =	 {November}
}

@PhdThesis{mika:phd01,
  author = 	 {Mika Katara},
  title = 	 {Aspects of Continuous Behaviour -- Design of Real-Time 
                  Reactive Systems in DisCo},
  school = 	 {Tampere University of Technology},
  year = 	 {2001},
  key =		 {2001},
  OPTaddress = 	 {},
  OPTtype = 	 {},
  OPTmonth = 	 {},
  thesistype =	 {PhD thesis},
  topics =       {2. Theses},  
  OPTannote =    {}
}

@InProceedings{pk:tphols01,
  author = 	 {Pertti Kellom{\"a}ki},
  title = 	 {A Structural Embedding of {O}csid in {PVS}},
  booktitle = 	 {Theorem Proving in Higher Order Logics, TPHOLS2001},
  OPTcrossref =  {},
  OPTkey = 	 {},
  pages =	 {281--296},
  year =	 {2001},
  editor = 	 {Richard J. Boulton and Paul B. Jackson},
  OPTvolume = 	 {},
  number =	 {2152},
  series =	 {Lecture Notes in Computer Science},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  publisher =	 {Springer Verlag},
  OPTannote = 	 {}
}

@InProceedings{mika+:iceccs01,
  author = 	 {Mika Katara and Tommi Mikkonen},
  title = 	 {Aspect-Oriented Specification Architectures for 
                  Distributed Real-Time Systems},
  booktitle = 	 {Proceedings of the Seventh IEEE International Conference on
                  Engineering of Complex Computer Systems, ICECCS 2001},
  OPTcrossref =  {},
  OPTkey = 	 {},
  pages = 	 {180--190},
  year = 	 {2001},
  editor = 	 {Sten F. Andler and Michael G. Hinchey and Jeff Offutt},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  address = 	 {Sk{\"o}vde, Sweden},
  month = 	 jun,
  OPTorganization = {},
  publisher =    {IEEE Computer Society Press},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{pk:dipes00,
  author = 	 {Pertti Kellom{\"a}ki},
  title = 	 {Deriving Message Passing Protocols From Collective 
                  Behavior},
  booktitle = 	 {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)},
  OPTcrossref =  {},
  OPTkey = 	 {},
  editor = 	 {Bernd Kleinjohann},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {2001},
  OPTorganization = {},
  publisher =	 {Kluwer Academic Publishers},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  pages =	 {183--192},
  OPTannote = 	 {}
}

@InProceedings{mika+:dipes00,
  author = 	 {Mika Katara and Arto Luoma},
  title = 	 {Environment Modelling in Closed Specifications of Embedded
                  Systems},
  booktitle = 	 {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)},
  OPTcrossref =  {},
  OPTkey = 	 {},
  editor = 	 {Bernd Kleinjohann},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {2001},
  OPTorganization = {},
  publisher =	 {Kluwer Academic Publishers},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  pages =	 {141--150},
  OPTannote = 	 {}
}

@Article{tta+:jucs01,
  author = 	 {Timo Aaltonen and Mika Katara and Risto Pitk{\"a}nen},
  title = 	 {{DisCo} Toolset -- The New Generation},
  journal = 	 {Journal of Universal Computer Science},
  year = 	 {2001},
  OPTkey = 	 {},
  volume = 	 {7},
  number = 	 {1},
  pages = 	 {3--18},
  OPTmonth = 	 {},
  note = 	 {http://www.jucs.org},
  sourceURL =    {http://www.jucs.org/jucs_7_1/disco_toolset_the_new},
  OPTannote = 	 {}
}

@Article{tta+:fac00,
  author = 	 {Timo Aaltonen and Pertti Kellom{\"a}ki and Risto Pitk{\"a}nen},
  title = 	 {Specifying Cash-Point with DisCo},
  journal = 	 {Formal Aspects of Computing},
  year = 	 {2000},
  OPTkey = 	 {},
  volume =	 {12},
  number =	 {4},
  pages =	 {231--232},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InCollection{mika:lncs1906,
  author =       "Mika Katara",
  title =        "Hybrid Models for Mobile Computing",
  booktitle =    "Coordination Languages and Models, 
                  4th International Conference, COORDINATION 2000, 
                  Proceedings",
  editor =       "Ant{\'o}nio Porto and Gruia-Catalin Roman",
  publisher =    "Springer--Verlag",
  series =       "Lecture Notes in Computer Science",
  number =       "1906",
  pages =        "216--231",
  year =         "2000",
  OPTannote =    ""
}

@InProceedings{rks+:wcc00,
  author = 	 {Reino Kurki-Suonio and Tommi Mikkonen},
  title = 	 {From Program Construction to Abstraction Engineering},
  booktitle = 	 {16th World Computer Congress 2000, Proceedings of 
                  Conference on Software: Theory and Practice},
  OPTcrossref =  {},
  OPTkey = 	 {},
  pages =	 {861--868},
  year =	 {2000},
  editor =	 {Yulin Feng and David Notkin and Marie-Claude Gaudel},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  address =	 {Beijing, China},
  month =	 aug,
  organization = {IFIP},
  publisher =	 {Publishing House of Electronics Industry and International 
                  Federation for Information Processing},
  OPTnote = 	 {},
}

@InProceedings{pk:wcc00,
  author = 	 {Pertti Kellom{\"a}ki},
  title = 	 {Verification-Friendly Specification of Distributed Systems},
  booktitle = 	 {16th World Computer Congress 2000, Proceedings of 
                  Conference on Software: Theory and Practice},
  OPTcrossref =  {},
  OPTkey = 	 {},
  pages =	 {480--483},
  year =	 {2000},
  editor =	 {Yulin Feng and David Notkin and Marie-Claude Gaudel},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  address =	 {Beijing, China},
  month =	 aug,
  organization = {IFIP},
  publisher =	 {Publishing House of Electronics Industry and International
                  Federation for Information Processing},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{timo+:wcc00,
  author =       {Timo Aaltonen and Mika Katara and Risto Pitk{\"a}nen},
  title =        {Verifying Real-Time Joint Action Specifications Using 
                  Timed Automata},
  booktitle = 	 {16th World Computer Congress 2000, Proceedings of 
                  Conference on Software: Theory and Practice},
  OPTcrossref =  {},
  OPTkey =       {},
  pages =        {516--525},
  year =         {2000},
  editor =       {Yulin Feng and David Notkin and Marie-Claude Gaudel},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  address =      {Beijing, China},
  month =        aug,
  organization = {IFIP},
  publisher =	 {Publishing House of Electronics Industry and International 
                  Federation for Information Processing},
  sourceURL =    {http://disco.cs.tut.fi/publications/papers/verifying.pdf},
  OPTannote =    {}
}


@InCollection{pk+:ecoop2000,
  author =       "Pertti Kellom{\"a}ki and Tommi Mikkonen",
  title =        "Design Templates for Collective Behavior",
  booktitle =    "Proceedings of ECOOP 2000, 14th European Conference on
                  Object-Oriented Programming",
  editor =       "Elisa Bertino",
  publisher =    "Springer--Verlag",
  series =       "Lecture Notes in Computer Science",
  number =       "1850",
  pages =        "277--295",
  year =         "2000",
  OPTannote =    ""
}

@InProceedings{mika+:rtc99,
  author =    {Mika Katara and Tommi Mikkonen},
  title =     {Design Approach for Real-Time Reactive Systems},
  booktitle = {Proceedings of the International Workshop on Real-Time 
               Constraints},
  editor =    {P.-A. Hsiung and F. Wang},
  month =     oct,
  year =      {1999},
  address =   {Alexandria, Virginia, USA},
  pages =     {11--20},
  sourceURL = {http://www.cs.ccu.edu.tw/~pahsiung/cp99-rtc/proceedings.html},
  OPTannote = {}
}  

@InProceedings{rks:fm99,
  author = 	 {Reino Kurki-Suonio},
  title = 	 {Component and Interface Refinement in Closed-System 
                  Specifications},
  booktitle = 	 {{FM}'99 -- Formal Methods: World Congress on Formal Methods 
                  in the Development of Computing Systems},
  OPTcrossref =  {},
  OPTkey = 	 {},
  editor =	 {J. Wing and J. Woodcock and J. Davies},
  number =	 {1708},
  series =	 {Lecture Notes in Computer Science},
  year =	 {1999},
  OPTorganization = {},
  publisher =	 {Springer--Verlag},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  pages =	 {134--154},
  OPTnote = 	 {},
  OPTannote =     {}
}

@InProceedings{pk+:fm99,
  author = 	 {Pertti Kellom{\"a}ki and Tommi Mikkonen},
  title = 	 {Archived Design Steps in Temporal Logic},
  booktitle = 	 {{FM}'99 -- Formal Methods: World Congress on Formal Methods 
                  in the Development of Computing Systems},
  OPTcrossref =  {},
  OPTkey = 	 {},
  pages =	 {1858--1858},
  OPTyear = 	 {},
  editor =	 {J. Wing and J. Woodcock and J. Davies},
  number =	 {1708},
  series =	 {Lecture Notes in Computer Science},
  year =	 {1999},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  publisher =	 {Springer--Verlag},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{mika:fusst99,
  author =    {Mika Katara},
  title =     {Composing {D}is{C}o Specifications Using Generic Real-Time
               Events -- A Mobile Robot Case Study},
  booktitle = {Software Technology, Proceedings of the Fenno-Ugric
                  Symposium {FUSST'99}},
  editor =    {Jaan Penjam},
  publisher = {Institute of Cybernetics at 
               Tallinn Technical University (Technical Report CS 104/99)},
  month =     aug,
  year =      {1999},
  address =   {Sagadi, Estonia},
  pages =     {75--86},
  sourceURL = {http://disco.cs.tut.fi/publications/papers/fusst99.pdf},
  OPTannote = {}
}  


@Article{rks+:csse99,
  author = {Reino Kurki-Suonio and Mika Katara},
  title = {Logical layers in specifications with distributed objects 
           and real time},
  journal = {Computer Systems Science \& Engineering},
  volume = {14},
  number = {4}, 
  pages = {217--226},
  month = jul,
  year = {1999},
  OPTannote = 	 {}
}

@InProceedings{risto+:pdpta99,
  author = 	 {Risto Pitk{\"a}nen and Harri Klapuri},
  title = 	 {Incremental Cospecification Using Objects and Joint Actions},
  booktitle = 	 {Proceedings of the International Conference on
                  Parallel and Distributed Processing Techniques and
                  Applications ({PDPTA'99})},
  editor =	 {H. R. Arabnia},
  year =	 1999,
  month =	 jun,
  volume =       "VI",
  pages =        "2961--2967",
  publisher =    "CSREA Press",
  OPTannote = 	 {}
}

@InProceedings{tjm:pdpta99,
  author = 	 {Tommi Mikkonen},
  title = 	 {Codesign Requires Closed-System Specifications},
  booktitle = 	 {Proceedings of the International Conference on
                  Parallel and Distributed Processing Techniques and
                  Applications ({PDPTA'99})},
  editor =	 {H. R. Arabnia},
  year =	 1999, 
  month =	 jun,
  volume =       "VI",
  pages =        "2968--2974",
  publisher =    "CSREA Press",
  OPTannote = 	 {}
}

@TechReport{disco99,
  author = 	 {Timo Aaltonen and Risto Pitkänen},
  title = 	 {Verifying Safety by Combining Joint Actions with a
                  Process-Algebraic Approach},
  institution =  {Tampere University of Technology, Software Systems Laboratory},
  year = 	 {1999},
  OPTkey = 	 {},
  OPTtype = 	 {},
  number =	 {19},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  sourceURL =    "http://disco.cs.tut.fi/reports/vscjapaa.ps",
  topics =       {3. Technical Reports},
  OPTannote = 	 {}
}

@PhdThesis{tjm:phd99,
  author = 	 {Tommi Mikkonen},
  title = 	 {Abstractions and Logical Layers in Specifications of
                  Reactive Systems},
  school = 	 {Tampere University of Technology},
  year = 	 {1999},
  key =		 {1999},
  OPTaddress = 	 {},
  OPTtype = 	 {},
  OPTmonth = 	 {},
  thesistype =	 {PhD thesis},
  topics =       {2. Theses},  
  OPTannote =    {}
}

@InCollection{rks+:ios99,
  author = 	 {Reino Kurki-Suonio and Tommi Mikkonen},
  booktitle = 	 {Information Modelling and Knowledge Bases X},
  title = 	 {Harnessing the power of interaction},
  publisher = 	 {IOS Press},
  year = 	 {1999},
  OPTkey = 	 {},
  editor =	 {H. Jaakkola and H. Kangassalo and E. Kawaguchi},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  pages =	 {1--11},
  OPTtype = 	 {},
  OPTnote = 	 {},
}		

@InProceedings{pk+:dipes98,
  author = 	 {Pertti Kellom{\"a}ki and Tommi Mikkonen},
  title = 	 {Modeling Distributed State as an Abstract Object},
  booktitle = 	 {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)},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {1999},
  OPTorganization = {},
  publisher =	 {Kluwer Academic Publishers},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  pages =	 {223--230},
  OPTnote = 	 {#137},
  OPTannote = 	 {}
}

@TechReport{disco98,
  author = 	 {Tommi Mikkonen},
  title = 	 {A Layer-Based Formalization of an On-Board Instrument},
  institution =  {Tampere University of Technology, Software Systems Laboratory},
  year = 	 {1998},
  OPTkey = 	 {},
  OPTtype = 	 {},
  number =	 {18},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  sourceURL =    "http://www.cs.tut.fi/~tjm/coala.ps",
  topics =       {3. Technical Reports},
  OPTannote = 	 {}
}

@InProceedings{rks+:ejcimkb98,
  author = 	 {Reino Kurki-Suonio and Tommi Mikkonen},
  title = 	 {Harnessing the Power of Interaction},
  booktitle = 	 {Proceedings of the 8th {E}uropean--{J}apanese
                  Conference on Information Modelling and Knowledge Bases},
  OPTcrossref =  {},
  OPTkey = 	 {},
  editor =	 {H. Jaakkola and H. Kangassalo},
  OPTvolume = 	 {},
  number =	 {A 19},
  series =	 {Series {A} -- Pori School of Technology and Economics},
  year =	 {1998},
  OPTorganization = {},
  OPTpublisher =    {},
  OPTaddress = 	 {},
  month =	 may,
  pages =	 {1-14},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{tjm:icse98,
  author = 	 {Tommi Mikkonen},
  title = 	 {Formalizing Design Patterns},
  booktitle = 	 {Proceedings of the 20th International Conference on
                 Software Engineering ({ICSE}'98)},
  OPTcrossref =  {},
  OPTkey = 	 {},
  editor =	 {B. Werner},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {1998},
  OPTorganization = {},
  publisher =	 {IEEE Computer Society},
  OPTaddress =	 {},
  month =	 apr,
  pages = 	 {115--124},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{tjm+:iwpse98,
  author = 	 {Tommi Mikkonen and Hannu-Matti J{\"a}rvinen},
  title = 	 {Specifying for Releases},
  booktitle = 	 {Proceedings of the International Workshop on
                  Principles of Software Evolution {IWPSE98}},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {1998},
  OPTorganization = {},
  OPTpublisher = {},
  OPTaddress = 	 {},
  month =	 apr,
  pages = 	 {118--122},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{rks+:pdse98,
  author = 	 {Reino Kurki-Suonio and Tommi Mikkonen},
  title = 	 {Abstractions of Distributed Cooperation, their
                  Refinement and Implementation},
  booktitle = 	 {Proceedings of the International Symposium on Software
                  Engineering for Parallel and Distributed Systems},
  OPTcrossref =  {},
  OPTkey = 	 {},
  editor =	 {B. Kr{\"a}mer and N. Uchihira and P. Croll and
                  S. Russo},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {1998},
  organization = {{IEEE} Computer Society},
  OPTpublisher = {},
  OPTaddress = 	 {},
  month =	 apr,
  pages =	 {94--102},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{rks+:isorc98,
  author =       {Reino Kurki-Suonio and Mika Katara},
  title =        {Real Time in a {TLA}-Based Theory of Reactive Systems},
  booktitle =    {Proceedings of the first IEEE International 
                  Symposium on Object-oriented Real-time distributed 
                  Computing}, 
  pages =        {186--195}, 
  month =        apr,
  year =         {1998},
  organization = {IEEE Computer Society},
  OPTannote =    {}
}

@InProceedings{tjm:ifip98,
  author =       {Tommi Mikkonen},
  title =        {A Development Cycle for Dependable Reactive Systems},
  booktitle =    {Proceedings of the 1998 International IFIP Workshop on 
                  Dependable Computing and Its Applications},
  editor =       {Y. Chen},
  pages =        {70--82},
  organization = {University of Witwatersrand},
  address =      {Johannesburg, South Africa},
  year =         {1998},
  sourceURL =    {http://www.cs.wits.ac.za/research/workshop/ifip98.html},
  OPTannote =    {}
}

@InCollection{rks+:lncs1357,
  author =       "Reino Kurki-Suonio and Tommi Mikkonen",
  title =        "Liberating Object-Oriented Modeling from Programming-Level
                  Abstractions",
  booktitle =    "Object-Oriented Technology, {ECOOP}'97 Workshop Reader",
  editor =       "J. Bosch and S. Mitchell",
  publisher =    "Springer--Verlag",
  series =       "Lecture Notes in Computer Science",
  number =       "1357",
  pages =        "195--199",
  year =         "1998",
  OPTannote =    ""
}


@PhdThesis{pk:phd97,
  author = 	 {Pertti Kellom{\"a}ki},
  title = 	 {Mechanical Verification of Invariant Properties of
                  {DisCo} Specifications},
  school = 	 {Tampere University of Technology},
  year = 	 {1997},
  key =		 {1997},
  OPTaddress = 	 {},
  OPTtype = 	 {},
  OPTmonth = 	 {},
  thesistype =	 {PhD thesis},
  annote =	 {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.},
  topics =        {2. Theses},  
  WWWannote =	 {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.},
  OPTannote =     {}
}


@MastersThesis{risto:msc97,
  author = 	 {Risto Pitk{\"a}nen},
  title = 	 {{DisCo}-spesifikaatioiden simulointi {J}avalla
                  ({S}imulation of {DisCo} Specifications in {J}ava)},
  school = 	 {Tampere University of Technology},
  year = 	 {1997},
  OPTkey = 	 {},
  OPTaddress = 	 {},
  thesistype = 	 {Master's thesis},
  month =	 jun,
  note =	 {In Finnish},
  topics = 	 {2. Theses},
  OPTannote =    {}
}


@InProceedings{pk:fme97,
  author = 	 {Pertti Kellom{\"a}ki},
  title = 	 {Verification of Reactive Systems Using {DisCo} and {PVS}},
  booktitle = 	 {{FME}'97: Industrial Applications and Strengthened
                  Foundations of Formal Methods},
  OPTcrossref =  {},
  OPTkey = 	 {},
  editor =	 {John Fitzgerald and Cliff B. Jones and Peter Lucas},
  OPTvolume = 	 {},
  number =	 {1313},
  series =	 {Lecture Notes in Computer Science},
  year =	 {1997},
  OPTorganization = {},
  publisher =	 {Springer--Verlag},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  pages =	 {589--604},
  OPTnote = 	 {},
  annote =	 {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.},
  WWWannote =	 {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.},
  OPTannote =     {}
}

@MastersThesis{mika:msc96,
  author = 	 {Mika Katara},
  title = 	 {Spesifikaatioiden strukturoinnista {TLA+}:ssa ja
                  {DisCossa} ({O}n structuring of specifications in {TLA+}
                  and {DisCo})},
  school = 	 {Tampere University of Technology},
  year = 	 {1996},
  month =        sep,
  OPTkey = 	 {},
  OPTaddress = 	 {},
  thesistype = 	 {Master's thesis},
  OPTmonth = 	 {},
  note =	 {In Finnish},
  topics =       {2. Theses},
  sourceURL =    {http://disco.cs.tut.fi/publications/papers/mikad.pdf},
  OPTannote = 	 {}
}

@InProceedings{pk:tphols96,
  author = 	 {Pertti Kellom{\"a}ki},
  title = 	 {Using Auxiliary Knowledge in Automating Invariant Proofs},
  booktitle = 	 {Supplementary Proceedings of the 9th International
                  Conference on Theorem Proving in Higher Order Logics:
                  TPHOLs'96},
  OPTcrossref =  {},
  OPTkey = 	 {},
  editor =	 {Joakim von Wright and Jim Grundy and John Harrison},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {1996},
  OPTorganization = {},
  publisher =	 {Turku Centre for Computer Science},
  OPTaddress = 	 {},
  month =	 aug,
  pages =	 {57--68},
  OPTnote = 	 {},
  annote =	 {Describes how invariant proofs of {DisCo}
                  specifications are partly automated by generating
                  strategies for the PVS theorem prover.},
  WWWannote =	 {Describes how invariant proofs of {DisCo}
                  specifications are partly automated by generating
                  strategies for the PVS theorem prover.},
  OPTannote = 	 {}
}

@InProceedings{pk:haifa96,
  author = 	 "Pertti Kellom{\"a}ki",
  title = 	 "Mechanical Verification of {D}is{C}o Specifications",
  OPTcrossref =  "",
  OPTkey = 	 "",
  OPTeditor = 	 "",
  OPTvolume = 	 "",
  OPTnumber = 	 "",
  OPTseries = 	 "",
  OPTpages = 	 "",
  booktitle =	 "{I}sraeli--{F}innish Binational Symposium on 
                  Specification, Development, and Verification of 
                  Concurrent Systems",
  year =	 "1996",
  OPTorganization = "",
  OPTpublisher = "",
  address =	 "The Technion, Haifa",
  month =	 jan,
  note =	 "http://www.cs.tut.fi/\verb|~|pk/papers.html",
  annote =	 "Describes verification of {DisCo} invariants in a
                  general level.",
  WWWannote =	 "Describes verification of {DisCo} invariants in a
                  general level.",
  sourceURL =     "http://www.cs.tut.fi/~pk/papers.html",
  OPTannote = 	 {}
}

@MastersThesis{tta:msc96,
  author = 	 {Timo Aaltonen},
  title = 	 {{DisCo}-kielen kehitt{\"a}misest{\"a} ({O}n developing the
                  {DisCo} language)},
  school = 	 {Tampere University of Technology},
  year = 	 {1996},
  OPTkey = 	 {},
  OPTaddress = 	 {},
  thesistype = 	 {Master's thesis},
  month =	 mar,
  note =	 {In Finnish},
  topics =       {2. Theses},
  OPTannote = 	 {}
}

@InCollection{rks:kluwer1996,
  author = 	 {Reino Kurki-Suonio},
  booktitle = 	 {Object-Oriented Behavioral Specifications },
  title = 	 {Fundamentals of object-oriented specification and 
                  modeling of collective behaviors},
  publisher = 	 {Kluwer Academic Publishers},
  year = 	 {1996},
  OPTkey = 	 {},
  editor =	 {H. Kilov and W. Harvey},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  pages =	 {101--120},
  OPTtype = 	 {},
  OPTnote = 	 {},
  annote =	 {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.},
  WWWannote =	 {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.},
  OPTannote = 	 {}
}

@InCollection{rks:lncs1169,
  author = 	 {Reino Kurki-Suonio},
  booktitle = 	 {Formal Systems Specification},
  title = 	 {Incremental specification with joint actions: 
                  the {RPC}-memory specification problem},
  publisher = 	 {Springer--Verlag},
  year = 	 {1996},
  OPTkey = 	 {},
  editor =	 {M. Broy and S. Merz and K. Spies},
  OPTvolume =	 {},
  number =	 {1169},
  series =	 {Lecture Notes in Computer Science},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  pages =	 {375--404},
  OPTtype = 	 {},
  OPTnote = 	 {},
  annote =	 {Uses the joint action approach to derive a solution 
                  to a specification problem. The volume contains 
                  various solutions using different specification 
                  techniques.},
  WWWannote =	 {Uses the joint action approach to derive a solution 
                  to a specification problem. The volume contains 
                  various solutions using different specification 
                  techniques.},
  OPTannote = 	 {}
}


@PhdThesis{ks:phd95,
  author = 	 {Kari Syst{\"a}},
  title = 	 {A Specification Method for Interactive Systems},
  school = 	 {Tampere University of Technology},
  year = 	 {1995},
  OPTkey = 	 {},
  OPTaddress = 	 {},
  thesistype = 	 {PhD thesis},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  topics =       {2. Theses},
  OPTannote = 	 {}
}

@InProceedings{pk:visegrad95,
  author = 	 "Pertti Kellom{\"a}ki",
  title = 	 "Mechanizing Invariant Proofs of Joint Action Systems",
  OPTcrossref =  "",
  OPTkey = 	 "",
  OPTeditor = 	 "",
  OPTvolume = 	 "",
  OPTnumber = 	 "",
  OPTseries = 	 "",
  pages = 	 "141--152",
  booktitle =	 "Proceedings of the Fourth Symposium on Programming 
                  Languages and Software Tools",
  year =	 "1995",
  OPTorganization = "",
  OPTpublisher = "",
  address =	 "Visegrad, Hungary",
  month =	 jun,
  note =	 "http://www.cs.tut.fi/\verb|~|pk/papers.html",
  annote =	 "Describes initial attempts for formalizing {DisCo} in
                  the PVS theorem prover and proving invariants.",
  WWWannote =	 "Describes initial attempts for formalizing {DisCo} in
                  the PVS theorem prover and proving invariants.",
  sourceURL =	 "http://www.cs.tut.fi/~pk/papers.html",
  OPTannote = 	 {}
}

@InProceedings{tjm:visegrad95,
  author = 	 {Tommi Mikkonen},
  title = 	 {An experimental code generator for implementing 
                  formal specifications given as closed systems},
  booktitle = 	 {Proceedings of the Fourth Symposium on Programming 
                  Languages and Software Tools},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {1995},
  OPTorganization = {},
  OPTpublisher = {},
  address =	 {Visegrad, Hungary},
  month =	 jun,
  OPTpages = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Misc{tjm:lictech95,
  OPTkey = 	 {},
  author =	 {Tommi Mikkonen},
  title =	 {Implementation of reactive systems based on 
                  closed-system specifications},
  howpublished = {Licentiate of Technology thesis, Tampere University
                  of Technology},
  year =	 {1995},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  topics =       {2. Theses},
  OPTannote = 	 {}
}

@InProceedings{tjm:iee95,
  author = 	 {Tommi Mikkonen},
  title = 	 {Partitioning {DisCo} specifications},
  booktitle = 	 {IEE Colloquium on Partitioning in hardware-software
                  codesigns},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {1995},
  OPTorganization = {},
  OPTpublisher = {},
  address =	 {London, United Kingdom},
  month =	 feb,
  OPTpages = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{pk:lyngby94,
  author = 	 "Pertti Kellom{\"a}ki",
  title = 	 "Self Stabilization of a Protocol",
  OPTcrossref =  "",
  OPTkey = 	 "",
  OPTeditor = 	 "",
  OPTvolume = 	 "",
  OPTnumber = 	 "",
  OPTseries = 	 "",
  OPTpages = 	 "",
  booktitle =	 "Proceedings of the Nordic Seminar on 
                  Dependable Computing Systems",
  year = 	 "1994",
  OPTorganization = "",
  OPTpublisher = "",
  address = 	 "Lyngby, Denmark",
  month = 	 "24.--26. August",
  note =	 "http://www.cs.tut.fi/\verb|~|pk/papers.html",
  annote =	 "A short version of~\cite{pk:lictech94}. Gives an
                  overview of the specification and verification of a
                  distributed token ring protocol.",
  WWWannote =	 "A short version of Pertti's licentiate thesis. Gives an
                  overview of the specification and verification of a
                  distributed token ring protocol.",
  sourceURL =	 "http://www.cs.tut.fi/~pk/papers.html",
  OPTannote = 	 {}
}

@Misc{pk:lictech94,
  OPTcrossref =  "",
  OPTkey = 	 "",
  author =	 "Pertti Kellom{\"a}ki",
  title =	 "Analysis of a Stabilizing Protocol",
  howpublished = "Licentiate of Technology thesis, Tampere University
		  of Technology",
  year =	 "1994",
  OPTmonth = 	 "",
  note =	 "http://www.cs.tut.fi/\verb|~|pk/papers.html",
  annote =	 "Gives a detailed {DisCo} specification of a
                  distributed token ring protocol, and a hand
                  verification of the stabilization properties of the
                  protocol.",
  WWWannote =	 "Gives a detailed {DisCo} specification of a
                  distributed token ring protocol, and a hand
                  verification of the stabilization properties of the
                  protocol.",
  sourceURL =	 "http://www.cs.tut.fi/~pk/papers.html",
  topics =       {2. Theses},
  OPTannote = 	 {}
}


@Article{rks:computer94,
  author = 	 {Reino Kurki-Suonio},
  title = 	 {Real time: further misconceptions or half-truths},
  journal = 	 {{IEEE} Computer},
  year = 	 {1994},
  OPTkey = 	 {},
  volume =	 {27},
  number =	 {6},
  month =	 jun,
  pages =	 {71--76},
  OPTnote = 	 {},
  annote =	 {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.},
  WWWannote =	 {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.},
  OPTannote = 	 {}
}


@Article{ks:sigchi94,
  author = 	 {Kari Syst{\"a}},
  title = 	 {Specifying User Interfaces in {DisCo}},
  journal = 	 {ACM SIGCHI Bulletin},
  year = 	 {1994},
  OPTkey = 	 {},
  volume =	 {26},
  number =	 {2},
  month =	 apr,
  pages =	 {53--58},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{ks:tartu93,
  author = 	 {Kari Syst{\"a}},
  title = 	 {Specifying User Interfaces as Joint Action Systems},
  booktitle = 	 {Proceedings of the Third Symposium on Programming
                  Languages and Software Tools},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {1993},
  organization = {University of Tartu},
  OPTpublisher = {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  pages =	 {130--141},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{tjm:fai93,
  author = 	 {Tommi Mikkonen},
  title = 	 {On implementing object-oriented specifications 
                  given as closed systems},
  booktitle = 	 {Conceptual Modeling and Object-Oriented Programming},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {1993},
  OPTorganization = {},
  publisher =	 {Finnish Artificial Intelligence Society},
  OPTaddress = 	 {},
  month =	 nov,
  OPTpages = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}


@InProceedings{hmj+:oopsla93,
  author = 	 {Hannu-Matti J{\"a}rvinen and Reino Kurki-Suonio and
                  Kari Syst{\"a}},
  title = 	 {Experiences in object-oriented modeling with
                  multi-object actions (invited lecture)},
  booktitle = 	 {Proceedings of the {OOPSLA}'93 Workshop on
                  Specification of Behavioral Semantics in
                  Object-Oriented Information Modeling},
  OPTcrossref =  {},
  OPTkey = 	 {},
  editor =	 {H. Kilov and B. Harvey},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {1993},
  OPTorganization = {},
  OPTpublisher = {},
  address =	 {Robert Morris College},
  OPTmonth = 	 {},
  pages =	 {61--66},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Article{rks+:scp93,
  author = 	 {R. Kurki-Suonio and K. Syst{\"a} and J. Vain},
  title = 	 {Real-time specification and modeling with joint actions},
  journal = 	 {Science of Computer Programming},
  year = 	 {1993},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  number =	 {20},
  month =	 apr,
  pages =	 {113--140},
  OPTnote = 	 {},
  annote =	 {Based on a workshop paper, where real-time 
                  specification with this approach was first discussed.},
  WWWannote =	 {Based on a workshop paper, where real-time 
                  specification with this approach was first discussed.},
  OPTannote = 	 {}
}

@InCollection{rks:lncs736,
  author = 	 {Reino Kurki-Suonio},
  booktitle = 	 {Hybrid Systems},
  title = 	 {Hybrid models with fairness and distributed clocks},
  publisher = 	 {Springer--Verlag},
  year = 	 {1993},
  OPTkey = 	 {},
  editor =	 {R.L. Grossman et al.},
  OPTvolume = 	 {},
  number =	 {736},
  series =	 {Lecture Notes in Computer Science},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  pages =	 {103--120},
  OPTtype = 	 {},
  OPTnote = 	 {},
  annote =	 {Analyzes how the approach can be used for 
                  real-time and hybrid systems.},
  WWWannote =	 {Analyzes how the approach can be used for 
                  real-time and hybrid systems.},
  OPTannote = 	 {}
}

@Article{rks:tse93,
  author =       "Reino Kurki-Suonio",
  title =        "Stepwise Design of Real-Time Systems",
  journal =      "IEEE Transactions on Software Engineering",
  pages =        "56--69",
  volume =       "19",
  number =       "1",
  month =        jan,
  year =         "1993",
  location =     "CMU E \&{} S Library",
  annote =       {Based on a SIGSOFT conference paper, where the 
                  design methodology of the approach was considered 
                  for real-time systems.},
  WWWannote =    {Based on a SIGSOFT conference paper, where the 
                  design methodology of the approach was considered 
                  for real-time systems.},
  OPTannote = 	 {}
}


@MastersThesis{tjm:msc92,
  author = 	 {Tommi Mikkonen},
  title = 	 {Formaalin määrittelyn toteutusperiaatteet},
  school = 	 {Tampere University of Technology},
  year = 	 {1992},
  OPTkey = 	 {},
  OPTaddress = 	 {},
  thesistype = 	 {Master's thesis},
  note =	 {In Finnish},
  topics =       {2. Theses},
  OPTannote = 	 {}
}


@PhdThesis{hmj:phd92,
  author = 	 {Hannu-Matti J{\"a}rvinen},
  title = 	 {The design of a specification language for reactive systems},
  school = 	 {Tampere University of Technology},
  year = 	 {1992},
  OPTkey = 	 {},
  OPTaddress = 	 {},
  OPTtype = 	 {},
  OPTmonth = 	 {},
  thesistype = 	 {PhD thesis},
  topics =       {2. Theses},
  OPTannote = 	 {}
}

@MastersThesis{manu:msc92,
  author = 	 {Manu Set{\"a}l{\"a}},
  title = 	 {Lentokoneen avioniikan formaali mallintaminen
                  ({F}ormal modeling of an avionics system)},
  school = 	 {Tampere University of Technology},
  year = 	 1992,
  OPTkey = 	 {},
  OPTaddress = 	 {},
  thesistype = 	 {Master's thesis},
  OPTmonth = 	 {},
  note =	 {In Finnish},
  topics =       {2. Theses},
  OPTannote = 	 {}
}

@MastersThesis{tm:msc92,
  author = 	 {Tatu M{\"a}nnisto},
  title = 	 {{DisCo}-spesifiointikielen virtuaalikone ({A}
                  virtual machine for the {DisCo} specification language)},
  school = 	 {Tampere University of Technology},
  year = 	 {1992},
  OPTkey = 	 {},
  OPTaddress = 	 {},
  thesistype = 	 {Master's thesis},
  OPTmonth = 	 {},
  note =	 {In Finnish},
  topics =       {2. Theses},
  OPTannote = 	 {}
}

@InProceedings{rks+:euromicro92,
  author = 	 {K. Syst{\"a} and R. Kurki-Suonio},
  title = 	 {Modeling of distributed real-time systems in {DisCo}},
  booktitle = 	 {Proceedings of the Fourth Euromicro Workshop on
                  Real-Time Systems},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {1992},
  OPTorganization = {},
  publisher =	 {{IEEE} Computer Society Press},
  address =	 {Athens, Greece},
  month =	 jun,
  pages =	 {136--141},
  OPTnote = 	 {},
  annote =	 {Discusses real-time modeling with the approach, with
                  an emphasis on using the {DisCo} tool},
  WWWannote =	 {Discusses real-time modeling with the approach, with
                  an emphasis on using the {DisCo} tool},
  OPTannote = 	 {}
}

@Article{rks:dc92,
  author = 	 {Reino Kurki-Suonio},
  title = 	 {Operational specification with joint actions:
                  serializable databases}, 
  journal = 	 {Distributed Computing},
  year = 	 {1992},
  OPTkey = 	 {},
  volume =	 {6},
  number =	 {1},
  month =	 jan,
  pages =	 {19--37},
  OPTnote = 	 {},
  annote =	 {Demonstrates incremental modeling with the
                  approach.},
  WWWannote =	 {Demonstrates incremental modeling with the
                  approach.},
  OPTannote = 	 {}
}

@InCollection{rks:ios92,
  author = 	 {Reino Kurki-Suonio},
  booktitle = 	 {Information Modelling and Knowledge Bases III},
  title = 	 {Modular modeling of temporal behaviors},
  publisher = 	 {IOS Press},
  year = 	 {1992},
  OPTkey = 	 {},
  editor =	 {S. Ohsuga et al.},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  pages =	 {283--300},
  OPTtype = 	 {},
  OPTnote = 	 {},
  annote =	 {Demonstrates incremental modeling using the 
                  "doctors' office" example.},
  WWWannote =	 {Demonstrates incremental modeling using the 
                  "doctors' office" example.},
  OPTannote = 	 {}
}		  

@Article{francez+:fac92,
  author = 	 "Nissim Francez and Ralph-J. J. Back and Reino Kurki-Suonio",
  title = 	 "On Equivalence-completions of Fairness Assumptions",
  OPTcrossref =  "",
  OPTkey = 	 "",
  journal =	 "Formal Aspects of Computing",
  year =	 "1992",
  volume =	 "6",
  number =	 "4",
  pages =	 "582--591",
  OPTmonth = 	 "",
  annote =	 "Analyzes such fairness notions in distributed 
                  systems that are not equivalence robust. 
                  Further development of ideas presented in an 
                  ICALP paper in 1988.",
  WWWannote =	 "Analyzes such fairness notions in distributed 
                  systems that are not equivalence robust. 
                  Further development of ideas presented in an 
                  ICALP paper in 1988.",
  OPTannote = 	 {}
}


@InProceedings{rks+:lncs571,
  author = 	 {R. Kurki-Suonio and K. Syst{\"a} and J. Vain},
  title = 	 {Scheduling in real-time models},
  booktitle = 	 {Formal Techniques in Real-Time and
                  Fault Tolerant Systems},
  OPTcrossref =  {},
  OPTkey = 	 {},
  editor =	 {J. Vytopil},
  OPTvolume = 	 {},
  number =	 {571},
  series =	 {Lecture Notes in Computer Science},
  year =	 {1991},
  OPTorganization = {},
  publisher =	 {Springer--Verlag},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  pages =	 {327--339},
  OPTnote = 	 {},
  annote =	 {Discusses real-time modeling with the approach.},
  WWWannote =	 {Discusses real-time modeling with the approach.},
  OPTannote = 	 {}
}

@InProceedings{ks:ewrts91,
  author = 	 {Kari Syst{\"a}},
  title = 	 {A Graphical Tool for Specification of Reactive Systems},
  booktitle = 	 {Proceedings of the Euromicro'91
                  Workshop on Real-Time Systems},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {1991},
  OPTorganization = {},
  publisher =	 {IEEE Computer Society Press},
  address =	 {Paris, France},
  month =	 jun,
  pages =	 {12--19},
  OPTnote = 	 {},
  annote =	 {Describes the animation tool.},
  WWWannote =	 {Describes the animation tool.},
  sourceURL =    {ftp://ftp.cs.tut.fi/pub/reports/disco_tool.ps},
  OPTannote = 	 {}
}

@InProceedings{hmj+:ieee91,
  author = 	 {Hannu-Matti J{\"a}rvinen and Reino Kurki-Suonio},
  title = 	 {{DisCo} specification language: marriage of 
                  actions and objects},
  booktitle = 	 {Proceedings of the 11th International Conference 
                  on Distributed Computing Systems},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {1991},
  OPTorganization = {},
  publisher =	 {IEEE Computer Society Press},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  pages =	 {142-151},
  OPTnote = 	 {},
  annote =	 {Discusses the {DisCo} language and design 
                  methodology in the light of the alternating 
                  bit protocol example},
  WWWannote =	 {Discusses the {DisCo} language and design 
                  methodology in the light of the alternating 
                  bit protocol example},
  OPTannote = 	 {}
}


@TechReport{disco90b,
  author = 	 {Hannu-Matti J{\"a}rvinen and Reino Kurki-Suonio},
  title = 	 {The {D}is{C}o Language and Temporal Logic of Actions},
  institution =  {Tampere University of Technology, Software Systems Laboratory},
  year = 	 {1990},
  OPTkey = 	 {},
  OPTtype = 	 {},
  number =	 {11},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  sourceURL =    "ftp://ftp.cs.tut.fi/pub/reports/rep11.ps",
  topics =       {3. Technical Reports},
  OPTannote = 	 {}
}

@TechReport{disco90a,
  author = 	 {Hannu-Matti J{\"a}rvinen and Reino Kurki-Suonio},
  title = 	 {The {D}is{C}o Language},
  institution =  {Tampere University of Technology, Software Systems Laboratory},
  year = 	 {1990},
  OPTkey = 	 {},
  OPTtype = 	 {},
  number =	 {8},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  topics =       {3. Technical Reports},
  OPTannote = 	 {}
}


@InProceedings{rks+:ieee90,
  author = 	 {H.-M. J{\"a}rvinen and R. Kurki-Suonio and 
                  M. Sakkinen and K. Syst{\"a}},
  title = 	 {Object-oriented specification of reactive systems},
  booktitle = 	 {Proceedings of the 12th International Conference 
                  on Software Engineering},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTeditor = 	 {},  
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {1990},
  OPTorganization = {},
  publisher =	 {IEEE Computer Society Press},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  pages =	 {63--71},
  OPTnote = 	 {},
  annote =	 {Supersedes~\cite{rks+:sen89}},
  WWWannote =	 {Supersedes the workshop paper that appeared in
                  Software Engineering Notes in 1989.},
  sourceURL =    {ftp://ftp.cs.tut.fi/pub/reports/icse12.ps},
  OPTannote = 	 {}
}


@Misc{ks:lictech90,
  author = 	 {Kari Syst{\"a}},
  title = 	 {Suoritettavien spesifikaatioiden visualisointi- ja
                  animointijärjestelmä ({V}isualization and Animation 
                  of Executable Specifications)},
  howpublished = {Licentiate of Technology thesis, Tampere University
                  of Technology},
  year = 	 {1990},
  note =         {In Finnish},
  topics =       {2. Theses},
  OPTannote = 	 {}
}


@MastersThesis{oae:msc90,
  author = 	 "Olavi Eerola",
  title = 	 "Suoritettavan spesifiointikielen kääntäjä ({A}
                  Compiler for an Executable Specification Language)",
  school = 	 "Tampere University of Technology",
  year = 	 1990,
  note =	 {In Finnish},
  thesistype =      {Master's thesis},
  topics =       {2. Theses},
  OPTannote = 	 {}
}


@Article{rks:ac90,
  author = 	 {Reino Kurki-Suonio},
  title = 	 {Towards languages that support program derivation, 
                  or control modularity considered harmful},
  journal = 	 {Acta Cybernetica},
  year = 	 {1990},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  number =	 {9},
  OPTmonth = 	 {},
  pages =	 {179-192},
  OPTnote = 	 {},
  annote =	 {Argues against using conventional control-based 
                  modularity in specification and design languages.},
  WWWannote =	 {Argues against using conventional control-based 
                  modularity in specification and design languages.},
  OPTannote = 	 {}
}


@Article{back+:dc89,
  author = 	 {R. J. R. Back and R. Kurki-Suonio},
  title = 	 {Decentralization of process nets with centralized control},
  journal = 	 {Distributed Computing},
  year = 	 {1989},
  OPTkey = 	 {},
  volume = 	 {3},
  number =	 {},
  OPTmonth = 	 {},
  pages =	 {73--87},
  OPTnote = 	 {},
  annote =	 {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.},
  WWWannote =	 {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.},
  OPTannote = 	 {}
}

@InProceedings{rks+:sen89,
  author = 	 {R. Kurki-Suonio and H.-M. J{\"a}rvinen},
  title = 	 {Action system approach to the specification and
                  design of distributed systems}, 
  booktitle = 	 {Proceedings of the 5th International Workshop on 
                  Software Specification and Design},
  series =       {ACM Software Engineering Notes},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  number =	 {14},
  OPTseries = 	 {},
  year =	 {1989},
  OPTorganization = {},
  OPTpublisher = {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  pages =	 {34--40},
  OPTnote = 	 {},
  annote =	 {The ideas of {DisCo} were first published here.},
  WWWannote =	 {The ideas of {DisCo} were first published here.},
  OPTannote = 	 {}
}


@InProceedings{back+:lncs317,
  author = 	 {R. J. R. Back and R. Kurki-Suonio},
  title = 	 {Serializability in distributed systems with handshaking},
  booktitle = 	 {Proceedings of ICALP 88},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  number =	 {317},
  series =	 {Lecture Notes in Computer Science},
  year =	 {1988},
  OPTorganization = {},
  publisher =	 {Springer--Verlag},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  pages =	 {52--66},
  OPTnote = 	 {},
  annote =	 {Analyzes the different fairness notions that are 
                  natural for action systems.},
  WWWannote =	 {Analyzes the different fairness notions that are 
                  natural for action systems.},
  OPTannote = 	 {}
}

@Article{back+:toplas88,
  author = 	 {R. J. R. Back and R. Kurki-Suonio},
  title = 	 {Distributed cooperation with action systems},
  journal = 	 {{ACM} Transactions on Programming Languages and Systems},
  year = 	 {1988},
  OPTkey = 	 {},
  volume = 	 {10},
  number =	 {4},
  month = 	 oct,
  pages =	 {513--554},
  OPTnote = 	 {},
  annote =	 {A basic paper about joint action systems.},
  WWWannote =	 {A basic paper about joint action systems.},
  OPTannote = 	 {}
}

@Article{rks+:bit88,
  author = 	 {R. Kurki-Suonio and T. Kankaanp{\"a}{\"a}},
  title = 	 {On the design of reactive systems},
  journal = 	 {{BIT}},
  year = 	 {1988},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  number =	 {28},
  OPTmonth = 	 {},
  pages =	 {581--604},
  OPTnote = 	 {},
  annote =	 {The specification of a simplified telephone 
                  exchange is discussed. Was written when the 
                  ideas of {DisCo} were still in early stages 
                  of development.},
  WWWannote =	 {The specification of a simplified telephone 
                  exchange is discussed. Was written when the 
                  ideas of {DisCo} were still in early stages 
                  of development.},
  OPTannote = 	 {}
} 


@InProceedings{rks:popl86,
  author = 	 {Reino Kurki-Suonio},
  title = 	 {Towards programming with knowledge expressions},
  booktitle = 	 {Proceedings of the ACM Conference on Principles of
                  Programming Languages},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  year =	 {1986},
  OPTorganization = {},
  publisher =	 {ACM},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  pages =	 {140--149},
  OPTnote = 	 {},
  annote =	 {Discusses development of distributed programs 
                  in terms of knowledge logic. Uses joint actions 
                  and the same example as the "Decentralization of 
                  process nets ..." paper.},
  WWWannote =	 {Discusses development of distributed programs 
                  in terms of knowledge logic. Uses joint actions 
                  and the same example as the "Decentralization of 
                  process nets ..." paper.},
  OPTannote = 	 {}
}


@Misc{disco-tutorial,
  OPTkey = 	 {},
  author =       {},
  title =	 {The {DisCo} Tutorial},
  OPTtitle = 	 {},
  howpublished = {At {URL} http://disco.cs.tut.fi on the
                  World Wide Web},
  year =         {1999},
  OPTyear = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  sourceURL =    {http://disco.cs.tut.fi},
  topics =       {4. Others},
  OPTannote = 	 {}
}

@Misc{disco-www,
  key =		 {9999},
  author =       {},
  title =	 {The {DisCo} project {WWW} page},
  howpublished = {At \url{http://disco.cs.tut.fi} on the World
                  Wide Web},
  year =         {2001},
  OPTyear = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  sourceURL =    {http://disco.cs.tut.fi},
  topics =       {4. Others},
  OPTannote = 	 {}
}