{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T03:54:50Z","timestamp":1725594890599},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540604068"},{"type":"electronic","value":"9783540455523"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60406-5_7","type":"book-chapter","created":{"date-parts":[[2011,7,5]],"date-time":"2011-07-05T19:52:06Z","timestamp":1309895526000},"page":"59-75","source":"Crossref","is-referenced-by-count":0,"title":["Using a symbolic model checker for verify safety properties in SA\/RT models"],"prefix":"10.1007","author":[{"given":"Javier","family":"Tuya","sequence":"first","affiliation":[]},{"given":"Luciano","family":"S\u00e1nchez","sequence":"additional","affiliation":[]},{"given":"Jose A.","family":"Corrales","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,8,18]]},"reference":[{"key":"7_CR1","unstructured":"Abadi, M., Lamport, L. (1993) \u201cConjoining Specifications\u201d. DEC Software Research Centre. Research Report no. 118"},{"issue":"no.1","key":"7_CR2","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/32.210305","volume":"19","author":"J. Atlee","year":"1993","unstructured":"Atlee, J., Gannon, J. (1993) \u201cState-Based Model Checking of Event-Driven System Requirements\u201d. IEEE Transactions on Software Engineering, Vol. 19, no. 1, January, pp. 24\u201340","journal-title":"IEEE Transactions on Software Engineering"},{"key":"7_CR3","volume-title":"Tech. Report UCB\/ERL M93\/71","author":"A. Aziz","year":"1993","unstructured":"Aziz, A., Tasiran, S., Brayton, K. (1993) \u201cBDD Variable Ordering for Interacting Finite State Machines\u201d. University of California, Berkeley. Tech. Report UCB\/ERL M93\/71"},{"issue":"no.8","key":"7_CR4","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. E. Bryant","year":"1986","unstructured":"Bryant, R. E. (1986) \u201cGraph-Based Algorithms for Boolean Function Manipulation\u201d. IEEE Transactions on Computers, Vol. 35, no. 8, August, pp. 677\u2013691","journal-title":"IEEE Transactions on Computers"},{"key":"7_CR5","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. R. Burch","year":"1992","unstructured":"Burch, J. R., Clarke, E. M., McMillan, K. L. Dill, D. L., Hwang, L. J. (1992) \u201cSymbolic Model Checking: 1020 States and Beyond\u201d. Information and Computation, Vol. 98, pp. 142\u2013170","journal-title":"Information and Computation"},{"key":"7_CR6","unstructured":"CCITT-Z.100 (1988) \u201cSDL Specification and Description Language (Blue Book)\u201d. CCITT"},{"issue":"no.2","key":"7_CR7","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"Clarke, E. M., Emerson, E. A., Sistla, A. P. (1986) \u201cAutomatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications\u201d. ACM Transactions on Programming Languages and Systems, Vol. 8, no. 2, April, pp. 244\u2013263","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"no.1","key":"7_CR8","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1109\/52.311049","volume":"11","author":"D. Craigen","year":"1994","unstructured":"Craigen, D., Gerhart, S., Talston, T. (1994) \u201cExperience with Formal Methods in Critical Systems: Regulatory Case Studies\u201d. IEEE Software, Vol. 11, no. 1, January, pp. 31\u201340","journal-title":"IEEE Software"},{"key":"7_CR9","unstructured":"Day, N. (1993) \u201cA Model Checker for Statecharts (Linking CASE Tools with Formal Methods)\u201d. MS Thesis, Univeristy of British Columbia, Department of Computer Science (Tech. Report 93-35)"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Dick, J., Loubersac, J. (1991) \u201cIntegrating Structured and Formal Methods: A Visual Approach to VDM\u201d. Proceedings of the 3rd European Software Engineering Conference, pp. 37\u201359","DOI":"10.1007\/3540547428_42"},{"issue":"no.2\/3","key":"7_CR11","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/BF01088591","volume":"5","author":"R. Elmstrom","year":"1993","unstructured":"Elmstrom, R., Lintulampi, R., Pezz\u00e9, M. (1993) \u201cGiving Semantics to SA\/RT by Means of High-Level Timed Petri Nets\u201d. Real-Time Systems Journal, Vol. 5, no. 2\/3, May, pp. 249\u2013271","journal-title":"Real-Time Systems Journal"},{"issue":"no.2","key":"7_CR12","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1109\/32.265634","volume":"20","author":"M. Felder","year":"1994","unstructured":"Felder, M., Mandrioli, D., Morzenti, A. (1994) \u201cProving Properties of Real-Time Systems Through Logical Specifications and Petri Net Models\u201d. IEEE Transactions on Software Engineering, Vol. 20, no. 2, pp. 127\u2013141","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"no.4","key":"7_CR13","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1109\/32.129221","volume":"18","author":"R. B. France","year":"1992","unstructured":"France, R. B. (1992) \u201cSemantically Extended Data Flow Diagrams: A Formal Specification Tool\u201d. IEEE Transactions on Software Engineering, Vol. 18, no. 4, April, pp. 329\u2013346","journal-title":"IEEE Transactions on Software Engineering"},{"key":"7_CR14","unstructured":"Graf, S., Steffen, B. (1991) \u201cCompositional Minimization of Finite State Systems\u201d. Tech. Report Aachener Informatikberichte, no. 91\u201323"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Harel, D. (1987) \u201cSTATECHARTS: A Visual Formalism for Complex Systems\u201d. Science of Computer Programming, North Holland, Vol. 8, pp. 231\u2013274","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"7_CR16","volume-title":"Strategies for Real Time System Specification","author":"D. J. Hatley","year":"1987","unstructured":"Hatley, D. J., Pirbhai, I. (1987) \u201cStrategies for Real Time System Specification\u201d. Dover Press, New York"},{"issue":"no.1","key":"7_CR17","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1109\/TSE.1980.230208","volume":"6","author":"K. Heninger","year":"1980","unstructured":"Heninger, K. (1980) \u201cSpecifying Software Requirements for Complex Systems: New Techniques and Their Applications\u201d. IEEE Transactions on Software Engineering, vol 6, no. 1, pp. 2\u201312","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"no.9","key":"7_CR18","doi-asserted-by":"crossref","first-page":"890","DOI":"10.1109\/TSE.1986.6313045","volume":"12","author":"F. Jahanian","year":"1986","unstructured":"Jahanian, F., Mok, A. K. (1986) \u201cSafety Analysis of Timing Properties in Real-Ttime Systems\u201d. IEEE Transactions on Software Engineering, Vol. 12, no. 9, September, pp. 890\u2013904","journal-title":"IEEE Transactions on Software Engineering"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Joyce, J. J., Seger, C. H. (1993) \u201cLinking BDD-Based Symbolic Evaluation to Interactive Theorem-Proving\u201d. Proceedings of the 30th Design automation Conference","DOI":"10.1145\/157485.164981"},{"issue":"no.7","key":"7_CR20","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1109\/MC.1993.274940","volume":"26","author":"N. G. Leveson","year":"1993","unstructured":"Leveson, N. G., Turner, C. S. (1993) \u201cAn Investigation of the Therac-25 Accidents\u201d. IEEE Computer, Vol. 26, no. 7, pp. 18\u201341","journal-title":"IEEE Computer"},{"issue":"no.9","key":"7_CR21","doi-asserted-by":"publisher","first-page":"684","DOI":"10.1109\/32.317428","volume":"20","author":"N. G. Leveson","year":"1994","unstructured":"Leveson, N. G., Heimdahl, M. P. E., Hildreth, H., Reese, J. D. (1994) \u201cRequirements Specification for Process Control Systems\u201d. IEEE Transactions on Software Engineering, Vol. 20, no. 9, pp. 684\u2013707","journal-title":"IEEE Transactions on Software Engineering"},{"key":"7_CR22","unstructured":"Lewerentz, C., Lindner, T. (eds.) (1994) \u201cCase Study \u201cProduction Cell\u201d. A Comparative Study in Formal Software Development\u201d. Forschungszentrum Informatik (FZI), Universit\u00e4t Karlsruhe."},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A. (1991) \u201cThe Temporal Logic of Reactive and Concurrent Systems: Specification\u201d. Springer-Verlag","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"7_CR24","unstructured":"McMillan, K. L. (1992) \u201cSymbolic Model Checking: An Approach to the State Explosion Problem\u201d. PhD. Thesis, Carnegie Mellon University (Tech. Report CMU-CS-92-131)"},{"issue":"no.2","key":"7_CR25","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1109\/32.214833","volume":"19","author":"G. Richter","year":"1993","unstructured":"Richter, G., Maffeo, B. (1993) \u201cTowards a Rigorous Interpretation of ESML \u2014 Extended Systems Modelling Language\u201d. IEEE Transactions on Software Engineering, Vol. 19, no. 2, Februray, pp. 165\u2013180","journal-title":"IEEE Transactions on Software Engineering"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Simone, R., Ressouche, A. (1994) \u201cCompositional semantics of Esterel and verification by compositional reductions\u201d. Proceedings of the Computer Aided Verification Conference, Springer-Verlag LNCS 818","DOI":"10.1007\/3-540-58179-0_74"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Tuya, J., S\u00e1nchez, L., Zurita, R., Corrales, J. A. (1993) \u201cA Pragmatic Task Design Approach Based on a Ward\/Mellor Real-Time Structured Specification\u201d. Proceedings of the 4th European Software Engineering Conference, pp. 301\u2013312","DOI":"10.1007\/3-540-57209-0_21"},{"key":"7_CR28","unstructured":"Tuya, J., Sevilla, L, S\u00e1nchez, L., Corrales, J. A. (1994) \u201cUsing Structured Methods in the Development of the User Interface Subsystem for a Reactive System\u201d. International Conference of Advanced Information Systems, Utretch. In Poster Outlines, pp. 14\u201316"},{"key":"7_CR29","unstructured":"Tuya, J. (1994) \u201cSpecification and Verification of Reactive Systems Using Structured Methods and Temporal Logic\u201d. Ph. D. Thesis, University of Oviedo (in Spanish)"},{"key":"7_CR30","unstructured":"Ward, P., Mellor, S. (1985) \u201cStructured Development for Real-Time Systems\u201d. Prentice-Hall"},{"issue":"no.2","key":"7_CR31","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TSE.1986.6312936","volume":"12","author":"P. Ward","year":"1986","unstructured":"Ward, P. (1986) \u201cThe Transformation Schema: An Extension of the Data Flow Diagram to Represent Control and Timing\u201d. IEEE Transactions on Software Engineering, Vol. 12, no. 2, pp. 198\u2013210","journal-title":"IEEE Transactions on Software Engineering"},{"key":"7_CR32","unstructured":"Xu, Q., Cau, A., Collette, P. (1994) \u201cOn Unifying Assumption-Commitment Style Proof Rules for Concurrency\u201d. Proceedings of CONCUR'94, Springer-Verlag LNCS 836"},{"key":"7_CR33","first-page":"1","volume":"3","author":"Q. Xu","year":"1994","unstructured":"Xu, Q., Roever, W. P., He J. (1994) \u201cRely-Guarantee Method for Verifying Shared Variable Concurrent Programs\u201d. Formal Aspects of Computing, Vol. 3, pp. 1\u201377","journal-title":"Formal Aspects of Computing"}],"container-title":["Lecture Notes in Computer Science","Software Engineering \u2014 ESEC '95"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60406-5_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T19:23:48Z","timestamp":1560367428000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60406-5_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540604068","9783540455523"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-60406-5_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}