{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:18:57Z","timestamp":1742617137803,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540616481"},{"type":"electronic","value":"9783540706533"}],"license":[{"start":{"date-parts":[[1996,1,1]],"date-time":"1996-01-01T00:00:00Z","timestamp":820454400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61648-9_32","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:10:12Z","timestamp":1330294212000},"page":"22-39","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Unifying verification paradigms"],"prefix":"10.1007","author":[{"given":"Natarajan","family":"Shankar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"2_CR1","volume-title":"IEEE Real-Time Technology and Applications Symp. (RTAS'96)","author":"M. Archer","year":"1996","unstructured":"M. Archer and C. Heitmeyer. Mechanical verification of timed automata: A case study. In IEEE Real-Time Technology and Applications Symp. (RTAS'96), Boston MA, June 1996. IEEE Computer Society Press. To Appear."},{"issue":"1","key":"2_CR2","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1109\/32.210305","volume":"19","author":"J. M. Atlee","year":"1993","unstructured":"Joanne M. Atlee and John Gannon. State-based model checking of event-driven system requirements. IEEE Transactions on Software Engineering, 19(1):24\u201340, January 1993.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2_CR3","first-page":"428","volume-title":"Symbolic model checking: 1020 states and beyond","author":"J. R. Burch","year":"1990","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. In 5th Annual IEEE Symposium on Logic in Computer Science, pages 428\u2013439, Philadelphia, PA, June 1990. IEEE Computer Society."},{"issue":"5","key":"2_CR4","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"Z. Chaochen","year":"1992","unstructured":"Zhou Chaochen, C. A. R. Hoare, and A. P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269\u2013276, 1992.","journal-title":"Information Processing Letters"},{"key":"2_CR5","first-page":"415","volume-title":"Computer-Aided Verification 94, volume 818 of Lecture Notes in Computer Science","author":"E. Clarke","year":"1994","unstructured":"E. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. In David Dill, editor, Computer-Aided Verification 94, volume 818 of Lecture Notes in Computer Science, pages 415\u2013427, Stanford, CA, June 1994. Springer Verlag."},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"E. M. Clarke and O. Grumberg. Research on automatic verication of finite state concurrent systems. In Annual Review of Computer Science, pages 269\u2013290. Annual Reviews, Inc., 1987.","DOI":"10.1146\/annurev.cs.02.060187.001413"},{"key":"2_CR7","volume-title":"Technical Report SRI-CSL-95-3","author":"D. Cyrluk","year":"1995","unstructured":"David Cyrluk, Patrick Lincoln, Steven Miller, Paliath Narendran, Sam Owre, Sreeranga Rajan, John Rushby, Natarajan Shankar, Jens Ulrik Skakkeb\u00e6k, Mandayam Srivas, and Friedrich von Henke. Seven papers on mechanized formal verification. Technical Report SRI-CSL-95-3, Computer Science Laboratory, SRI International, Menlo Park, CA, January 1995."},{"key":"2_CR8","volume-title":"Lecture Notes in Computer Science","author":"B. Dutertre","year":"1996","unstructured":"Bruno Dutertre. Elements of mathematical analysis in PVS. In International Conference on Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science, Turku, Finland, August 1996. Springer-Verlag. To appear."},{"key":"2_CR9","first-page":"84","volume-title":"Efficient model checking in fragments of the propositional mu-calculus","author":"E.A. Emerson","year":"1985","unstructured":"E.A. Emerson and C.L Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proceedings of the 10th Symposium on Principles of Programming Languages, pages 84\u201396, New Orleans, LA, January 1985. Association for Computing Machinery."},{"key":"2_CR10","volume-title":"The NRL Software Cost Reduction (SCR*) requirements specification methodology","author":"S. Faulk","year":"1987","unstructured":"S. Faulk and P. Clements. The NRL Software Cost Reduction (SCR*) requirements specification methodology. In Fourth International Workshop on Software Specification and Design, Monterey, CA, April 1987. IEEE Computer Society."},{"key":"2_CR11","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1007\/978-1-4612-3658-0_10","volume-title":"Current Trends in Hardware Verification and Theorem Proving","author":"M. J. C. Gordon","year":"1989","unstructured":"Michael J. C. Gordon. Mechanizing programming logics in higher-order logic. In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Theorem Proving, pages 387\u2013439, New York, NY, 1989. Springer-Verlag."},{"key":"2_CR12","first-page":"662","volume-title":"Formal Methods Europe FME '96, number 1051 in Lecture Notes in Computer Science","author":"K. Havelund","year":"1996","unstructured":"Klaus Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. In Formal Methods Europe FME '96, number 1051 in Lecture Notes in Computer Science, pages 662\u2013681, Oxford, UK, March 1996. Springer-Verlag."},{"key":"2_CR13","first-page":"79","volume-title":"Experiences and lessons from the analysis of TCAS II","author":"M. P. E. Heimdahl","year":"1996","unstructured":"Mats P. E. Heimdahl. Experiences and lessons from the analysis of TCAS II. In Steven J. Zeil, editor, International Symposium on Software Testing and Analysis (ISSTA), pages 79\u201383, San Diego, CA, January 1996. Association for Computing Machinery."},{"issue":"6","key":"2_CR14","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1109\/32.508311","volume":"22","author":"M. P. E. Heimdahl","year":"1996","unstructured":"Mats P. E. Heimdahl and Nancy G. Leveson. Completeness and consistency in hierarchical state-based requirements. IEEE Transactions on Software Engineering, 22(6):363\u2013377, June 1996.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Constance Heitmeyer, Alan Bull, Carolyn Gasarch, and Bruce Labaw. SCR*: A toolset for specifying and analyzing requirements. In COMPASS [22], pages 109\u2013122.","DOI":"10.1109\/CMPASS.1995.521891"},{"key":"2_CR16","volume-title":"Consistency checking of SCR*-style requirements specifications","author":"C. Heitmeyer","year":"1995","unstructured":"Constance Heitmeyer, Bruce Labaw, and Daniel Kiskis. Consistency checking of SCR*-style requirements specifications. In International Symposium on Requirements Engineering, York, England, March 1995. IEEE Computer Society."},{"issue":"1","key":"2_CR17","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1109\/TSE.1980.230208","volume":"SE-6","author":"K. L. Heninger","year":"1980","unstructured":"K. L. Heninger. Specifying software requirements for complex systems: New techniques and their application. IEEE Transactions on Software Engineering, SE-6(1):2\u201313, January 1980.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2_CR18","unstructured":"K. L. Heninger et al. Software requirements for the A-7E aircraft. NRL Report 3876, Naval Research Laboratory, November 1978."},{"key":"2_CR19","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/3-540-58468-4_158","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 863 of Lecture Notes in Computer Science","author":"J. Hooman","year":"1994","unstructured":"Jozef Hooman. Correctness of real time systems by construction. In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 863 of Lecture Notes in Computer Science, pages 19\u201340, L\u00fcbeck, Germany, September 1994. Springer-Verlag."},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"D. N. Hoover and Zewei Chen. Tablewise, a decision table tool. In COMPASS [22], pages 97\u2013108.","DOI":"10.1109\/CMPASS.1995.521890"},{"key":"2_CR21","unstructured":"John Hopcroft and Jeffrey Ullman. Introduction to Automata Theory, Languages, and Computation. Addison Wesley, 1979."},{"key":"2_CR22","unstructured":"COMPASS '95 (Proceedings of the Ninth Annual Conference on Computer Assurance), Gaithersburg, MD, June 1995. IEEE Washington Section."},{"key":"2_CR23","first-page":"69","volume-title":"Applying a mechanized duration calculus assistant","author":"R. Inal","year":"1994","unstructured":"Recep Inal and Jens U. Skakkeb\u00e6k. Applying a mechanized duration calculus assistant. In Hans Rischel, editor, Nordic Seminar on Dependable Computing Systems, pages 69\u201380, Lyngby, Denmark, August 1994. Technical University of Denmark."},{"key":"2_CR24","unstructured":"G. Janssen. ROBDD Software. Department of Electrical Engineering, Eindhoven University of Technology, October 1993."},{"key":"2_CR25","volume-title":"Mechanical verification of DisCo specifications","author":"P. Kellom\u00e4ki","year":"1996","unstructured":"Pertti Kellom\u00e4ki. Mechanical verification of DisCo specifications. In Israeli-Finnish Binational Symposium on Specification, Development, and Verification of Concurrent Systems, Haifa, Israel, January 1996. The Technion."},{"issue":"9","key":"2_CR26","doi-asserted-by":"crossref","first-page":"684","DOI":"10.1109\/32.317428","volume":"20","author":"N. G. Leveson","year":"1994","unstructured":"Nancy G. Leveson, Mats Per Erik Heimdahl, Holly Hildreth, and Jon Damon Reese. Requirements specification for process-control systems. IEEE Transactions on Software Engineering, 20(9):684\u2013707, September 1994.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2_CR27","first-page":"292","volume-title":"Computer-Aided Verification, CAV '93, volume 697 of Lecture Notes in Computer Science","author":"P. Lincoln","year":"1993","unstructured":"Patrick Lincoln and John Rushby. Formal verification of an algorithm for interactive consistency under a hybrid fault model. In Costas Courcoubetis, editor, Computer-Aided Verification, CAV '93, volume 697 of Lecture Notes in Computer Science, pages 292\u2013304, Elounda, Greece, June\/July 1993. Springer-Verlag."},{"key":"2_CR28","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems, Volume 1: Specification","author":"Z. Manna","year":"1992","unstructured":"Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems, Volume 1: Specification. Springer-Verlag, New York, NY, 1992."},{"key":"2_CR29","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. L. McMillan","year":"1993","unstructured":"Kenneth L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1993."},{"issue":"2","key":"2_CR30","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, February 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2_CR31","volume-title":"Technical Report SRI-CSL-95-12","author":"S. Owre","year":"1995","unstructured":"Sam Owre, John Rushby, and Natarajan Shankar. Analyzing tabular and statetransition specifications in PVS. Technical Report SRI-CSL-95-12, Computer Science Laboratory, SRI International, Menlo Park, CA, July 1995. Available, with specification files, from http:\/\/www.csl.sri.com\/csl-95-12.html"},{"key":"2_CR32","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0304-3975(76)90022-0","volume":"3","author":"David Park","year":"19","unstructured":"David Park. Finiteness is mu-ineffable. Theoretical Computer Science, 3:173\u2013181, 19.","journal-title":"Theoretical Computer Science"},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"2_CR34","first-page":"84","volume-title":"Computer-Aided Verification, CAV '95, volume 939 of Lecture Notes in Computer Science","author":"S. Rajan","year":"1995","unstructured":"S. Rajan, N. Shankar, and M.K. Srivas. An integration of model-checking with automated proof checking. In Pierre Wolper, editor, Computer-Aided Verification, CAV '95, volume 939 of Lecture Notes in Computer Science, pages 84\u201397, Liege, Belgium, June 1995. Springer-Verlag."},{"key":"2_CR35","volume-title":"Computer-Aided Verification, CAV '96, Lecture Notes in Computer Science","author":"H. Rue\u00df","year":"1996","unstructured":"H. Rue\u00df, N. Shankar, and M.K. Srivas. Modular verification of SRT division. In R. Alur and T.A. Henzinger, editors, Computer-Aided Verification, CAV '96, Lecture Notes in Computer Science, New Brunswick, NJ, July 1996. Springer-Verlag. To appear."},{"key":"2_CR36","doi-asserted-by":"crossref","unstructured":"Lance Sherry. A structured approach to requirements specification for softwarebased systems using operational procedures. In 13th AIAA\/IEEE Digital Avionics Systems Conference, pages 64\u201369, Phoenix, AZ, October 1994.","DOI":"10.1109\/DASC.1994.369502"},{"key":"2_CR37","volume-title":"Technical Report SRI-CSL-93-10","author":"J. U. Skakkeb\u00e6k","year":"1993","unstructured":"Jens U. Skakkeb\u00e6k and N. Shankar. A Duration Calculus proof checker: Using PVS as a semantic framework. Technical Report SRI-CSL-93-10, Computer Science Laboratory, SRI International, Menlo Park, CA, December 1993."},{"key":"2_CR38","volume-title":"PhD thesis","author":"J. U. Skakkeb\u00e6k","year":"1994","unstructured":"Jens Ulrik Skakkeb\u00e6k. A Verification Assistant for a Real-Time Logic. PhD thesis, Department of Computer Science, Technical University of Denmark, Lyngby, Denmark, November 1994."},{"key":"2_CR39","series-title":"Prentice Hall International Series in Computer Science","first-page":"125","volume-title":"Applications of Formal Methods","author":"M. K. Srivas","year":"1995","unstructured":"Mandayam K. Srivas and Steven P. Miller. Formal verification of the AAMP5 microprocessor. In Michael G. Hinchey and Jonathan P. Bowen, editors, Applications of Formal Methods, Prentice Hall International Series in Computer Science, chapter 7, pages 125\u2013180. Prentice Hall, Hemel Hempstead, UK, 1995."},{"key":"2_CR40","series-title":"volume B: Formal Models and Semantics","volume-title":"Handbook of Theoretical Computer Science","year":"1990","unstructured":"Jan van Leeuwen, editor. Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics. Elsevier and MIT press, Amsterdam, The Netherlands, and Cambridge, MA, 1990."}],"container-title":["Lecture Notes in Computer Science","Formal Techniques in Real-Time and Fault-Tolerant Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61648-9_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:23:51Z","timestamp":1742599431000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61648-9_32"}},"subtitle":["Extended abstract"],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540616481","9783540706533"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/3-540-61648-9_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]},"assertion":[{"value":"2 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}