{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T14:23:40Z","timestamp":1761488620525},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540231677"},{"type":"electronic","value":"9783540302063"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30206-3_3","type":"book-chapter","created":{"date-parts":[[2011,1,18]],"date-time":"2011-01-18T10:19:15Z","timestamp":1295345955000},"page":"5-20","source":"Crossref","is-referenced-by-count":9,"title":["Formal Verification of an Avionics Sensor Voter Using SCADE"],"prefix":"10.1007","author":[{"given":"Samar","family":"Dajani-Brown","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Darren","family":"Cofer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amar","family":"Bouali","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Caspi, P., Curic, A., Maignan, A., Sofronis, C., Tripakis, S., Niebert, P.: From Simulink to SCADE\/Lustre to TTA: a layered approach for distributed embedded applications. In: Proc. of the 2003 ACM SIGPLAN conference on Language, compiler, and tool for embedded systems, San Diego, USA (2003)","DOI":"10.1145\/780732.780754"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The Synchronous Data Flow Programming Language Lustre. Proceeding of the IEEE (September 1991)","DOI":"10.1109\/5.97300"},{"key":"3_CR3","volume-title":"Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST 1993, Workshop in Computing","author":"N. Halbwachs","year":"1993","unstructured":"Halbwachs, N., Lagnier, F., Raymond, P.: Synchronous observers and the verification of reactive systems. In: Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST 1993, Workshop in Computing, Springer, Heidelberg (1993)"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Sheeran, M., Stalmarck, G.: A tutorial on Stalmarck\u2019s proof procedure for propositional logic, Prover Technology AB and Chalmers University of Technology, Sweden (1998)","DOI":"10.1007\/3-540-49519-3_7"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Bjesse, P., Claessen, K.: SAT-based Verification without State Space Traversal. In: Formal Methods in Computer-Aided Design (2000)","DOI":"10.1007\/3-540-40922-X_23"},{"key":"3_CR6","volume-title":"Model Checking Software, 10th International SPIN Workshop","author":"S. Dajani-Brown","year":"2003","unstructured":"Dajani-Brown, S., Cofer, D., Hartmann, G., Pratt, S.: Formal Modeling and Analysis of an Avionics Triplex Sensor Voter. In: Model Checking Software, 10th International SPIN Workshop, May 2003, Springer, Heidelberg (2003)"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Berry, G., Bouali, A., Fornari, X., Ledinot, E., Nassor, E., de Simone, R.: ESTEREL: a formal method applied to avionic software development. Science of Computer Programming 36(1) (January 2000)","DOI":"10.1016\/S0167-6423(99)00015-5"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Osder, S.: Practical View of Redundancy Management Application and Theory. Journal of Guidance and Control 22(1) (January-February1999)","DOI":"10.2514\/2.4363"},{"key":"3_CR9","volume-title":"Introduction to Avionics","author":"R.P.G. Collinson","year":"1998","unstructured":"Collinson, R.P.G.: Introduction to Avionics. Chapman & Hall, London (1998)"},{"key":"3_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. McMillan","year":"1993","unstructured":"McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers, Boston (1993)"},{"key":"3_CR11","volume-title":"Huth and Mark D Ryan, Logic in Computer Science Modelling and reasoning about systems","author":"R.A. Micheal","year":"2000","unstructured":"Micheal, R.A.: Huth and Mark D Ryan, Logic in Computer Science Modelling and reasoning about systems. University Press, Cambridge (2000)"},{"key":"3_CR12","unstructured":"SMV web page, http:\/\/www-2.cs.cmu.edu\/~modelcheck"},{"key":"3_CR13","unstructured":"Simulink weg page, http:\/\/www.mathworks.com\/products\/simulink"},{"key":"3_CR14","unstructured":"SCADE 4.1.1, Training Manual, Esterel Technologies, Montreal, Canada"},{"key":"3_CR15","unstructured":"SCADE 4.2, Design Verifier User Manual, Esterel Technologies, Montreal, Canada"},{"key":"3_CR16","unstructured":"Berry, G.: The effectiveness of Synchronous Languages for the Development of Safety-Critical Systems. white paper, Esterel Technologies (2003)"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-24730-2_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2004","unstructured":"Ball, T., Levin, V., Xei, F.: Automatic Creation of Environment Models via Training. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 93\u2013107. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30206-3_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:48:38Z","timestamp":1605761318000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30206-3_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540231677","9783540302063"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30206-3_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}