{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T15:14:34Z","timestamp":1743002074355,"version":"3.40.3"},"publisher-location":"Boston, MA","reference-count":25,"publisher":"Springer US","isbn-type":[{"type":"print","value":"9781441915382"},{"type":"electronic","value":"9781441915399"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-1-4419-1539-9_13","type":"book-chapter","created":{"date-parts":[[2010,3,2]],"date-time":"2010-03-02T00:26:11Z","timestamp":1267489571000},"page":"381-428","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Model Checking Information Flow"],"prefix":"10.1007","author":[{"given":"Michael W.","family":"Whalen","sequence":"first","affiliation":[]},{"given":"David A.","family":"Greve","sequence":"additional","affiliation":[]},{"given":"Lucas G.","family":"Wagner","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,1,23]]},"reference":[{"year":"1999","author":"S Bensalem","key":"13_CR1_13","unstructured":"Bensalem S, Caspi P, Parent-Vigouroux C, Dumas C (1999) A methodology for proving control systems with Lustre and PVS. In: Proceedings of the seventh working conference on dependable computing for critical applications (DCCA 7), San Jose, January 1999"},{"key":"13_CR2_13","volume-title":"Model checking","author":"EM Clarke","year":"1999","unstructured":"Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT, Cambridge, MA"},{"key":"13_CR3_13","doi-asserted-by":"crossref","unstructured":"Cola\u00e7o JL, Girault A, Hamon G, Pouzet M (2004) Towards a higher-order synchronous data-flow language. In ACM fourth international conference on embedded software (EMSOFT\u201904), Pisa, Italy, September 2004","DOI":"10.1145\/1017753.1017792"},{"key":"13_CR4_13","unstructured":"Esterel Technologies, Inc. SCADE Suite product description. http:\/\/www.esterel-technologies.com\/products\/scade-suite"},{"key":"13_CR5_13","first-page":"11","volume-title":"IEEE symposium on security and privacy","author":"Goguen JA, Meseguer J (1982) Security policies and security models. In: Proceedings of the","year":"1982","unstructured":"Goguen JA, Meseguer J (1982) Security policies and security models. In: Proceedings of the 1982 IEEE symposium on security and privacy. IEEE Computer Society Press, Washington, DC, pp 11\u201320"},{"key":"13_CR6_13","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-1-4419-1539-9_9","volume-title":"Design and verification of microprocessor systems for high-assurance applications","author":"D Greve","year":"2010","unstructured":"Greve D (2010) Information security modeling and analysis. In: Hardin D (ed) Design and verification of microprocessor systems for high-assurance applications. Springer, Berlin, pp 249\u2013299"},{"issue":"9","key":"13_CR7_13","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N Halbwachs","year":"1991","unstructured":"Halbwachs N, Caspi P, Raymond P, Pilaud D (1991) The Synchronous dataflow programming language lustre. Proc IEEE 79(9):1305\u20131320","journal-title":"Proc IEEE"},{"key":"13_CR8_13","unstructured":"IRST http:\/\/nusmv.irst.itc.it\/ The NuSMV model checker, IRST, Trento, Italy"},{"key":"13_CR9_13","doi-asserted-by":"publisher","first-page":"1321","DOI":"10.1109\/5.97301","volume":"79","author":"P Le Guernic","year":"1991","unstructured":"Le Guernic P, Gautier T, Borgne ML, Maire CL (1991) Programming real-time applications with signal. Proc IEEE 79:1321\u20131336","journal-title":"Proc IEEE"},{"key":"13_CR10_13","doi-asserted-by":"crossref","first-page":"37","DOI":"10.3233\/JCS-1992-1103","volume":"1","author":"J MacLean","year":"1992","unstructured":"MacLean J (1992) Proving noninterference and functional correctness using traces. J Comput Secur 1:37\u201357","journal-title":"J Comput Secur"},{"key":"13_CR11_13","unstructured":"The Mathworks, Inc., Simulink and stateflow product description. http:\/\/www.mathworks.com\/Simulink, http:\/\/www.mathworks.com\/products\/stateflow\/"},{"key":"13_CR12_13","doi-asserted-by":"crossref","unstructured":"McMillan K (1998) Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In: Proceedings of the tenth international conference on computer aided verification (CAV\u201998) Vancouver, Canada, June 1998","DOI":"10.1007\/BFb0028738"},{"key":"13_CR13_13","doi-asserted-by":"crossref","unstructured":"McMillan K (1999) Circular compositional reasoning about liveness. In: Advances in hardware design and verification: IFIP WG10.5 international conference on correct hardware design and verification methods (CHARME\u201999), pp 342\u2013345","DOI":"10.1007\/3-540-48153-2_30"},{"key":"13_CR14_13","unstructured":"Munoz C (2009) ProofLite product description. http:\/\/research.nianet.org\/~munoz\/ProofLite"},{"key":"13_CR15_13","doi-asserted-by":"crossref","unstructured":"Owre S, Rushby JM, Shankar N (1992) PVS: a prototype verification system. In: 11th International conference on automated deduction (CADE), vol 607, Saratoga, NY, June 1992, pp 748\u2013752","DOI":"10.1007\/3-540-55602-8_217"},{"key":"13_CR16_13","unstructured":"Prover Technologies, Inc. Prover SL\/DE plug-in product description. http:\/\/www.prover.com\/products\/prover_plugin"},{"key":"13_CR17_13","unstructured":"Reactive Systems, Inc. Reactis product description. http:\/\/www.reactive-systems.com"},{"key":"13_CR18_13","unstructured":"Rockwell Collins Turnstile Product Page. http:\/\/www.rockwellcollins.com\/products\/gov\/airborne\/cross-platform\/information-assurance\/cross-domain-solutions\/index.html"},{"key":"13_CR19_13","doi-asserted-by":"crossref","unstructured":"Roscoe AW, Goldsmith MH (1999) What is intransitive noninterference? In: Proceedings of the 12th IEEE computer security foundations workshop, pp 228\u2013238","DOI":"10.1109\/CSFW.1999.779776"},{"key":"13_CR20_13","unstructured":"Rushby J (1992) Noninterference, transitivity, and channel-control security policies. Technical report csl-92\u20132, SRI"},{"key":"13_CR21_13","unstructured":"Ryan PYA (1991) A CSP formulation of non-interference. In: Cipher. IEEE Computer Society Press, Washington, DC, pp 19\u201327"},{"key":"13_CR22_13","unstructured":"SRI, Incorporated. PVS specification and verification system. http:\/\/pvs.csl.sri.com"},{"key":"13_CR23_13","unstructured":"SRI, SAL home page. http:\/\/www.csl.sri.com\/projects\/sal\/"},{"key":"13_CR24_13","doi-asserted-by":"crossref","unstructured":"Whalen M, Cofer D, Miller S, Krogh B, Storm W (2007) Integration of formal analysis into a model-based software development process. In: 12th International workshop on industrial critical systems (FMICS 2007), Berlin, Germany, July 2007","DOI":"10.1007\/978-3-540-79707-4_7"},{"key":"13_CR25_13","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-1-4419-1539-9_6","volume-title":"Design and verification of microprocessor systems for high-assurance applications","author":"M Wilding","year":"2010","unstructured":"Wilding M, Greve D, Richards R, Hardin D (2010) Formal verification of partition management for the AAMP7G microprocessor. In: Hardin D (ed) Design and verification of microprocessor systems for high-assurance applications. Springer, Berlin, pp 175\u2013191"}],"container-title":["Design and Verification of Microprocessor Systems for High-Assurance Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4419-1539-9_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,18]],"date-time":"2025-02-18T22:45:50Z","timestamp":1739918750000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-1-4419-1539-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9781441915382","9781441915399"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-1-4419-1539-9_13","relation":{},"subject":[],"published":{"date-parts":[[2010]]},"assertion":[{"value":"23 January 2010","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}