{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:58:14Z","timestamp":1725490694987},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540403340"},{"type":"electronic","value":"9783540449195"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44919-1_13","type":"book-chapter","created":{"date-parts":[[2007,9,3]],"date-time":"2007-09-03T00:38:42Z","timestamp":1188779922000},"page":"161-180","source":"Crossref","is-referenced-by-count":4,"title":["Specification and Validation of the SACI-1 On-Board Computer Using Timed-CSP-Z and Petri Nets"],"prefix":"10.1007","author":[{"given":"Adnan","family":"Sherif","sequence":"first","affiliation":[]},{"given":"Augusto","family":"Sampaio","sequence":"additional","affiliation":[]},{"given":"S\u00e9rgio","family":"Cavalcante","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,5,27]]},"reference":[{"key":"13_CR1","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"13th International Conference on Application and Theory pf Petri Nets","author":"G. Balbo","year":"1992","unstructured":"G. Balbo. Performance Issues in Parallel Programming. In 13th International Conference on Application and Theory pf Petri Nets, volume 616, pages 1\u201323, Sheffield, UK, 1992. Lecture Notes in Computer Science."},{"issue":"5","key":"13_CR2","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"C. Zhou","year":"1991","unstructured":"Zhou Chaochen, C. A. R. Hoare, and Anders P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269\u2013276, 1991.","journal-title":"Information Processing Letters"},{"issue":"2","key":"13_CR3","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/0304-3975(94)00169-J","volume":"138","author":"J. Davies","year":"1995","unstructured":"J. Davies and S. Schneider. A brief history of timed csp. Theoretical Computer Science, 138(2):243\u2013271, 1995.","journal-title":"Theoretical Computer Science"},{"key":"13_CR4","unstructured":"A. R. de Paula Jr. Fault Tolerance Aspects of the SACI-1. VI Simp\u00f3sio de Computadores Tolerantes a Falhas, 1995."},{"key":"13_CR5","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1007\/3-540-55092-5_22","volume":"571","author":"C.J. Finge","year":"1992","unstructured":"C.J. Finge. Specification and verification of real-time behaviors using z and rtl. Lecture Notes in Computer Science, 571:393\u2013409, 1992.","journal-title":"Lecture Notes in Computer Science"},{"key":"13_CR6","unstructured":"C. Fischer. Combining CSP and Z. Technical report, University of Oldenburg, 1996."},{"key":"13_CR7","unstructured":"C. Fischer. Combination and implementation of processes and data: from csp-oz to java. PhD thesis, University of Oldenburg, 2000."},{"key":"13_CR8","unstructured":"Formal Systems (Europe) Ltd. FDR: User Manual and Tutorial, version 2.01, August 1996."},{"issue":"2","key":"13_CR9","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1109\/32.67597","volume":"17","author":"C. Ghezzi","year":"1991","unstructured":"C. Ghezzi, D. Mandrioli, S. Morasca, and M. Pezze. A Unified High-level Petri Net Formalism for Time-Critical Systems. IEEE Transactions on Software Engineering, 17(2):160\u2013172, 1991.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"13_CR10","unstructured":"C. Ghezzi and M. Pezze. Cabernet: an environment for the specification and verification of real-time systems. In In Proceedings of 1992 DECUS Europe Symposium, Cannes (F), 1992."},{"key":"13_CR11","unstructured":"F. Jahanian, A. K. Mok, and D. A. Stuart. Formal specification of real-time systems. Technical Report TR-88-25, Department of Computer Science, University of Texas at Austin, June 1988."},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"B. Mahony and J. Song Dong. Blending Object-Z and Timed CSP: An introduction to TCOZ. In Proceedings of the 1998 Internaltional Conference on Software Engineering, pages 95\u2013104, 1998.","DOI":"10.1109\/ICSE.1998.671106"},{"issue":"3","key":"13_CR13","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1093\/comjnl\/41.3.145","volume":"41","author":"A. Mazzeo","year":"1998","unstructured":"A. Mazzeo, N. Mazzocca, S. Russo, C. Savy, and V. Vittorini. Formal Specification of Concurrent Systems: A Structured Approach. The Computer Journal, 41(3):145\u2013162, 1998.","journal-title":"The Computer Journal"},{"issue":"1","key":"13_CR14","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/S0167-6423(00)00023-X","volume":"40","author":"A. Mota","year":"2001","unstructured":"A. Mota and A. Sampaio. Model-Checking CSP-Z, Strategy, Tool Support and Industrial Application. Science of Computer Programing, 40(1):59\u201396, 2001.","journal-title":"Science of Computer Programing"},{"key":"13_CR15","unstructured":"J. A. C. F. Neri. SACI-1: A Cost-Effective Microssatellite Bus for Multiple Mission Payloads. Technical report, Instituto Nacional de Pesquisas Espaciais-INPE, 1995."},{"key":"13_CR16","unstructured":"B. Potter, J. Sinclair, and D. Till. An Introduction to Formal Specification and Z. Prentice-Hall, 1991."},{"key":"13_CR17","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of ICALP\u2019 86","author":"G. M. Reed","year":"1986","unstructured":"G. M. Reed and A. W. Roscoe. A timed model for communication sequential processes. In Proceedings of ICALP\u2019 86, volume 226. Lecture Notes in Computer Science, 1986."},{"issue":"5","key":"13_CR18","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1093\/logcom\/2.5.557","volume":"2","author":"A. W. Roscoe","year":"1992","unstructured":"A. W. Roscoe. An alternative order for the failures model. Journal of Logic and Computation, 2(5):557\u2013578, 1992.","journal-title":"Journal of Logic and Computation"},{"key":"13_CR19","unstructured":"A. W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall International, 1998."},{"key":"13_CR20","unstructured":"M. E. Saturno and J. B. Neto. Software Requirement Specification for the OBC\/SACI-1 Application Programs. Technical report, Instituto Nacional de Pesquisas Espaciais-INPE, 1995."},{"key":"13_CR21","unstructured":"A. Sherif. Formal Specification and Validation of Real-Time Systems. Master\u2019s thesis, Centro de Inform\u00e1tica, UFPE, 2000. http:\/\/www.di.ufpe.br\/~ams\/tese.ps.gz."},{"key":"13_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/3-540-45251-6_16","volume-title":"Proceedings of Formal Methods Europe 2001: Formal Methods for Increasing Software Productivity","author":"A. Sherif","year":"2001","unstructured":"A. Sherif, A. Sampaio, and S. Cavalcante. An Integrated Approach to Specification and Validation of Real-Time Systems. In Proceedings of Formal Methods Europe 2001: Formal Methods for Increasing Software Productivity, Lecture Notes in Computer Science, volume 2021, pages 278\u2013299. Springer, 2001."},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"C. Suhl. RT-Z: An Integration of Z and timed CSP. In Proceedings of the 1st Internaltional Conference on Integrated Formal Methods, 1999.","DOI":"10.1007\/978-1-4471-0851-1_3"}],"container-title":["Lecture Notes in Computer Science","Applications and Theory of Petri Nets 2003"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44919-1_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,23]],"date-time":"2019-02-23T10:13:57Z","timestamp":1550916837000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44919-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540403340","9783540449195"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-44919-1_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}