Теория процессов
 Скачать 1.62 Mb.
|
335[58] R.J. van Glabbeek: The linear time – branching time spectrum I. The semantics of concrete, sequential processes. In [42], pp. 3–100, 2001. [59] R.J. van Glabbeek and W.P. Weijland: Branching time and abstraction in bisimulation semantics. Journal of the ACM, 43:555–600, 1996. [60] N. G¨ otz, U. Herzog, and M. Rettelbach: Multiprocessor and distributed system design: The integration of functional specification and performance analysis using stochastic process algebras. In L. Donatiello and R. Nelson, editors, Performance Evaluation of Computer and Communication Systems, number 729 in LNCS, pages 121–146. Springer, 1993. [61] J.F. Groote: Process Algebra and Structured Operational Semantics. PhD thesis, University of Amsterdam, 1991. [62] J.F. Groote and B. Lisser: Computer assisted manipulation of algebraic process specifications. Technical Report SEN- R0117, CWI, Amsterdam, 2001. [63] J.F. Groote and M.A. Reniers: Algebraic process verification. In [42], pp. 1151–1208, 2001. [64] H. Hansson: Time and Probability in Formal Design of Distributed Systems. PhD thesis, University of Uppsala, 1991. [65] M. Hennessy: Algebraic Theory of Processes. MIT Press, 1988. [66] M. Hennessy and R. Milner: On observing nondeterminism and concurrency. In J.W. de Bakker and J. van Leeuwen, editors, Proceedings 7th ICALP, number 85 in Lecture Notes in Computer Science, pages 299– 309. Springer Verlag, 1980. [67] M. Hennessy and G.D. Plotkin: Full abstraction for a simple parallel programming language. In J. Becvar, editor, Proceedings MFCS, number 74 in LNCS, pages 108– 120. Springer Verlag, 1979. 336 [68] T.A. Henzinger, P. Ho, and H. Wong-Toi: Hy-Tech: The next generation. In Proceedings RTSS, pages 56–65. IEEE, 1995. [69] J. Hillston: A Compositional Approach to Performance Modelling. PhD thesis, Cambridge University Press, 1996. [70] C.A.R. Hoare: An axiomatic basis for computer programming. Communications of the ACM, 12:576–580, 1969. [71] C.A.R. Hoare: Communicating sequential processes. Communications of the ACM, 21(8):666–677, 1978. [72] C.A.R. Hoare: A model for communicating sequential processes. In R.M. McKeag and A.M. Macnaghten, editors, On the Construction of Programs, pages 229–254. Cambridge University Press, 1980. [73] C.A.R. Hoare: Communicating Sequential Processes. Prentice Hall, 1985. [74] K.G. Larsen, P. Pettersson, and Wang Yi: Uppaal in a nutshell. Journal of Software Tools for Technology Transfer, 1, 1997. [75] P. Linz: An Introduction to Formal Languages and Automata. Jones and Bartlett, 2001. [76] G. Lowe: Probabilities and Priorities in Timed CSP. PhD thesis, University of Oxford, 1993. [77] N. Lynch, R. Segala, F. Vaandrager, and H.B. Weinberg: Hybrid I/O automata. In T. Henzinger, R. Alur, and E. Sontag, editors, Hybrid Systems III, number 1066 in Lecture Notes in Computer Science. Springer Verlag, 1995. [78] S. MacLane and G. Birkhoff: Algebra. MacMillan, 1967. [79] S. Mauw: PSF: a Process Specification Formalism. PhD thesis, University of Amsterdam, 1991. http://carol.science.uva.nl/psf/ 337 [80] A. Mazurkiewicz: Concurrent program schemes and their interpretations. Technical Report DAIMI PB-78, Aarhus University, 1977. [81] J. McCarthy: A basis for a mathematical theory of computation. In P. Braffort and D. Hirshberg, editors, Computer Programming and Formal Systems, pages 33–70. North-Holland, Amsterdam, 1963. [82] G.J. Milne: CIRCAL: A calculus for circuit description. Integration, 1:121–160, 1983. [83] G.J. Milne and R. Milner: Concurrent processes and their syntax. Journal of the ACM, 26(2):302–321, 1979. [84] R. Milner: An approach to the semantics of parallel programs. In Proceedings Convegno di informatica Teoretica, pages 285– 301, Pisa, 1973. Instituto di Elaborazione della Informazione. [85] R. Milner: Processes: A mathematical model of computing agents. In H.E. Rose and J.C. Shepherdson, editors, Proceedings Logic Colloquium, number 80 in Studies in Logic and the Foundations of Mathematics, pages 157–174. North-Holland, 1975. [86] R. Milner: Algebras for communicating systems. In Proc. AFCET/SMF joint colloquium in Applied Mathematics, Paris, 1978. [87] R. Milner: Synthesis of communicating behaviour. In J. Winkowski, editor, Proc. 7th MFCS, number 64 in LNCS, pages 71–83, Zakopane, 1978. Springer Verlag. [88] R. Milner: Flowgraphs and flow algebras. Journal of the ACM, 26(4):794–818, 1979. [89] R. Milner: A Calculus of Communicating Systems. Number 92 in Lecture Notes in Computer Science. Springer Verlag, 1980. [90] R. Milner: Calculi for synchrony and asynchrony. Theoretical Computer Science, 25:267–310, 1983. 338 [91] R. Milner: A complete inference system for a class of regular behaviours. Journal of Computer System Science, 28:439–466, 1984. [92] R. Milner: Communication and Concurrency. Prentice Hall, 1989. [93] R. Milner: Calculi for interaction. Acta Informatica, 33:707– 737, 1996. [94] R. Milner: Communicating and Mobile Systems: the π- Calculus. Cambridge University Press, ISBN 052164320, 1999. http://www.cup.org/titles/ catalogue.asp?isbn=0521658691 [95] R. Milner: Bigraphical reactive systems. In K.G. Larsen and M. Nielsen, editors, Proceedings CONCUR ’01, number 2154 in LNCS, pages 16–35. Springer Verlag, 2001. [96] O. Jensen and R. Milner Bigraphs and Mobile Processes. Technical report, 570, Computer Laboratory, University of Cambridge, 2003. http://citeseer.ist.psu.edu/ jensen03bigraphs.html http://citeseer.ist.psu.edu/668823.html [97] R. Milner, J. lParrow, and D. Walker: A calculus of mobile processes. Information and Computation, 100:1–77, 1992. [98] F. Moller and P. Stevens: Edinburgh Concurrency Workbench user manual (version 7.1). http://www.dcs.ed.ac.uk/home/cwb/ [99] F. Moller and C. Tofts: A temporal calculus of communicating systems. In J.C.M. Baeten and J.W. Klop, editors, Proceedings CONCUR’90, number 458 in LNCS, pages 401–415. Springer Verlag, 1990. 339 [100] X. Nicollin and J. Sifakis: The algebra of timed processes ATP: Theory and application. Information and Computation, 114:131– 178, 1994. [101] D.M.R. Park: Concurrency and automata on infinite sequences. In P. Deussen, editor, Proceedings 5th GI Conference, number 104 in LNCS, pages 167–183. Springer Verlag, 1981. [102] C.A. Petri: Kommunikation mit Automaten. PhD thesis, Institut fuer Instrumentelle Mathematik, Bonn, 1962. [103] C.A. Petri: Introduction to general net theory. In W. Brauer, editor, Proc. Advanced Course on General Net Theory, Processes and Systems, number 84 in LNCS, pages 1–20. Springer Verlag, 1980. [104] G.D. Plotkin: A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus University, 1981. [105] G.D. Plotkin: The origins of structural operational semantics. Journal of Logic and Algebraic Programming, Special Issue on Structural Operational Semantics, 2004. [106] A. Pnueli: The temporal logic of programs. In Proceedings 19th Symposium on Foundations of Computer Science, pages 46–57. IEEE, 1977. [107] G.M. Reed and A.W. Roscoe: A timed model for communicating sequential processes. Theoretical Computer Science, 58:249–261, 1988. [108] M. Rem: Partially ordered computations, with applications to VLSI design. In J.W. de Bakker and J. van Leeuwen, editors, Foundations of Computer Science IV, volume 159 of Mathematical Centre Tracts, pages 1–44. Mathematical Centre, Amsterdam, 1983. 340 [109] S.A. Schneider: Concurrent and Real-Time Systems (the CSP Approach). Worldwide Series in Computer Science. Wiley, 2000. [110] D.S. Scott and C. Strachey: Towards a mathematical semantics for computer languages. In J. Fox, editor, Proceedings Symposium Computers and Automata, pages 19– 46. Polytechnic Institute of Brooklyn Press, 1971. [111] Y.S. Usenko: Linearization in µCRL. PhD thesis, Technische Universiteit Eindhoven, 2002. [112] B. Victor: A Verification Tool for the Polyadic π-Calculus. Licentiate thesis, Department of Computer Systems, Uppsala University, Sweden, May 1994. Report DoCS 94/50. [113] T.A.C. Willemse: Semantics and Verification in Process Algebras with Data and Timing. PhD thesis, Technische Universiteit Eindhoven, 2003. [114] Wang Yi: Real-time behaviour of asynchronous agents. In J.C.M. Baeten and J.W. Klop, editors, Proceedings CONCUR’90, number 458 in LNCS, pages 502– 520. Springer Verlag, 1990. [115] L. Wischik: New directions in implementing the π-calculus. University of Bologna, August 2002. http://www.fairdene.com/picalculus/ implementing-pi-c.pdf [116] S. Yovine: Kronos: A verification tool for real-time systems. Journal of Software Tools for Technology Transfer, 1:123–133, 1997. [117] D. Zhang, R. Cleaveland, and E. Stark: The integrated CWB-NC/PIOAtool for functional verification and performance analysis of concurrent systems. In H. Garavel and J. Hatcliff, editors, Proceedings TACAS’03, number 2619 in Lecture Notes in Computer Science, pages 431–436. Springer-Verlag, 2003. 341 [118] E. Clarke, O. Grumberg, D. Peled: Model checking. MIT Press, 2001. [119] J.Esparza: Decidability of model-checking for infinite-state concurrent systems, Acta Informatica, 34:85-107, 1997. [120] P.A.Abdulla, A.Annichini, S.Bensalem, A.Bouajjani, P.Habermehl, Y.Lakhnech: Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis, Lecture Notes in Computer Science 1633, pages 146-159, Springer-Verlag, 1999. [121] K.L.McMillan: Verification of Infinite State Systems by Compositional Model Checking, Conference on Correct Hardware Design and Verification Methods, pages 219-234, 1999. [122] O.Burkart, D.Caucal, F.Moller, and B.Steffen: Verification on infinite structures, In J. Bergstra, A. Ponse and S. Smolka, editors, Handbook of Process Algebra, chapter 9, pages 545-623, Elsevier Science, 2001. [123] D. Lee and M. Yannakakis. Principles and Methods of Testing Finite State Machines - a Survey. The Proceedings of the IEEE, 84(8), pp 1090-1123, 1996. [124] G. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs, N.J., first edition, 1991. [125] G. Holzmann. The SPIN Model Checker - Primer and Reference Manual. Addison-Wesley, 2003. [126] S. Huang, D. Lee, and M. Staskauskas. Validation-Based Test Sequence Generation for Networks of Extended Finite State Machines. In Proceedings of FORTE/PSTV, October 1996. [127] J. J. Li and M. Segal. Abstracting Security Specifications in Building Survivable Systems. In Proceedings of 22-тв National Information Systems Security Conference, October 1999, Arlington, Virginia, USA. 342 [128] Y.- J. Byun, B. A. Sanders, and C.-S. Keum. Design Patterns of Communicating Extended Finite State Machines in SDL . In Proceedings of 8-th Conference on Pattern Languages of Programs (PLoP’2001), September 2001, Monticello, Illinois, USA. [129] J. J. Li and W. E. Wong. Automatic Test Generation from Communicating Extended Finite State Machine (CEFSM)- Based Models. In Proceedings of the Fifth IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC’02), pp. 181-185, 2002. [130] S. Chatterjee. EAI Testing Automation Strategy. In Proceedings of 4-th QAI Annual International Software Testing Conference in India, Pune, India, February 2004 [131] ITU Telecommunication Standardization Sector (ITU-T), Recommendation Z.100, CCITT Specification and Description Language (SDL), Geneva 1994. [132] Information Processing Systems - Open Systems Interconnection: Estelle, A Formal Description Technique Based on Extended State Transition Model, ISO International Standard 9074, June 1989. [133] ISOIEC. LOTOS - A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. International Standard 8807, 1988. [134] D. Harel. A Visual Formalism for Complex Systems. Science of Computer Programming, 8:231-274, 1987. [135] D. Harel and A. Naamad. The STATEMATE semantics of statecharts. ACM Transactions on Software Engineering and Methodology (Also available as technical report of Weizmann Institute of Science, CS95-31), 5(4):293-333, Oct 1996. [136] M. Bozga, J. C. Fernandez, L. Ghirvu, S. Graf, J. P. Krimm, and L. Mounier. IF: An intermediate representation and validation environment for timed asynchronous systems. In 343 Proceedings of Symposium on Formal Methods 99, Toulouse, number 1708 in LNCS. Springer Verlag, September 1999. [137] M. Bozga, S. Graf, and L. Mounier. IF-2.0: A validation environment for componentbased real-time systems. In Proceedings of Conference on Computer Aided Verification, CAV’02, Copenhagen, LNCS. Springer Verlag, June 2002. [138] M. Bozga, D. Lesens, and L. Mounier. Model-Checking Ariane-5 Flight Program. In Proceedings of FMICS’01, Paris, France, pages 211-227. INRIA, 2001. [139] M. Bozga, S. Graf, and L. Mounier. Automated validation of distributed software using the IF environment. In 2001 IEEE International Symposium on Network Computing and Applications (NCA 2001). IEEE, October 2001. [140] M. Bozga and Y. Lakhnech. IF-2.0 common language operational semantics. Technical report, 2002. Deliverable of the IST Advance project, available from the authors. [141] http://www-128.ibm.com/developerworks/ library/specification/ws-bpel/ [142] http://www.bpml.org [143] http://www.wfmc.org/standards/docs/ better_maths_better_processes.pdf [144] http://www.fairdene.com/picalculus/ [145] http://www.bpmi.org/bpmi-library/ 2B6EA45491.workflow-is-just-a-pi-process.pdf [146] http://www.fairdene.com/picalculus/ bpm3-apx-theory.pdf [147] http://www.bpm3.com [148] http://portal.acm.org/citation.cfm?id=1223649 [149] http://www.w3.org/TR/ws-cdl-10/ 344 |