{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T11:15:43Z","timestamp":1763810143569,"version":"3.37.3"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030324407"},{"type":"electronic","value":"9783030324414"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[[2019]]},"DOI":"10.1007\/978-3-030-32441-4_8","type":"book-chapter","created":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T23:03:06Z","timestamp":1569193386000},"page":"111-131","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["On Teaching Applied Formal Methods in Aerospace Engineering"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6718-2828","authenticated-orcid":false,"given":"Kristin Yvonne","family":"Rozier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,9,23]]},"reference":[{"issue":"1","key":"8_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-009-0131-4","volume":"12","author":"YA Ameur","year":"2010","unstructured":"Ameur, Y.A., Boniol, F., Wiels, V.: Toward a wider use of formal methods for aerospace systems design and verification. Int. J. Softw. Tools Technol. Transf. 12(1), 1\u20137 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-540-87698-4_22","volume-title":"Computer Safety, Reliability, and Security","author":"N Basir","year":"2008","unstructured":"Basir, N., Denney, E., Fischer, B.: Constructing a safety case for automatically generated code from formal program verification information. In: Harrison, M.D., Sujan, M.-A. (eds.) SAFECOMP 2008. LNCS, vol. 5219, pp. 249\u2013262. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-87698-4_22"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-48119-2_22","volume-title":"FM\u201999 \u2014 Formal Methods","author":"P Behm","year":"1999","unstructured":"Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: M\u00e9t\u00e9or: a successful application of B in a large project. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 369\u2013387. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48119-2_22"},{"key":"8_CR4","unstructured":"B\u00e9rard, B., et al.: Systems and Software Verification: Model-checking Techniques and Tools. Springer, Heidelberg (2013). https:\/\/www.amazon.com\/Systems-Software-Verification-Model-Checking-Techniques\/dp\/3642074782\/ref=sr_1_1?ie=UTF8&qid=1483572091&sr=8-1&keywords=systems+and+software+verification"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-319-12214-4_7","volume-title":"Model-Based Safety and Assessment","author":"B Bittner","year":"2014","unstructured":"Bittner, B., et al.: An integrated process for FDIR design in aerospace. In: Ortmeier, F., Rauzy, A. (eds.) IMBSA 2014. LNCS, vol. 8822, pp. 82\u201395. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-12214-4_7"},{"key":"8_CR6","unstructured":"Butler, R., et al.: NASA\/NIA PVS Class 2012. NIA, Hampton, Virginia, USA, October 9\u201312 (2012). https:\/\/shemesh.larc.nasa.gov\/PVSClass2012\/online.html"},{"key":"8_CR7","unstructured":"Butler, R., Maddalon, J., Geser, A., Mu\u00f1oz, C.: Simulation and verification I: formal analysis of air traffic management systems: the case of conflict resolution and recovery. In: Proceedings of the 35th Conference on Winter Simulation: Driving Innovation, pp. 906\u2013914. Winter Simulation Conference (2003)"},{"key":"8_CR8","unstructured":"CENELEC, EN50126: Railway applications-the specification and demonstration of reliability. Availability, Maintainability and Safety (RAMS) (2001). https:\/\/www.cenelec.eu\/standardsdevelopment\/ourproducts\/europeanstandards.html"},{"key":"8_CR9","unstructured":"CENELEC, EN50128: Railway applications-communication, signaling and processing systems-software for railway control and protection systems (2011). https:\/\/www.cenelec.eu\/standardsdevelopment\/ourproducts\/europeanstandards.html"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Denney, E., Pai, G., Pohl, J.: Heterogeneous aviation safety cases: integrating the formal and the non-formal. In: 2012 IEEE 17th International Conference on Engineering of Complex Computer Systems, pp. 199\u2013208. IEEE (2012)","DOI":"10.1109\/ICECCS20050.2012.6299215"},{"key":"8_CR11","unstructured":"EN50129, CENELEC: Railway applications-communication, signalling and processing systems-safety related electronic systems for signalling. British Standards Institution, United Kingdom. ISBN, pp. 0580\u20134181 (2003)"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1007\/978-3-642-54862-8_54","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Essen von","year":"2014","unstructured":"von Essen, C., Giannakopoulou, D.: Analyzing the next generation airborne collision avoidance system. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 620\u2013635. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_54"},{"key":"8_CR13","unstructured":"Fisher, M.: An introduction to practical formal methods using temporal logic, vol. 82. Wiley Online Library (2011). https:\/\/www.amazon.com\/Introduction-Practical-Formal-Methods-Temporal-ebook\/dp\/B005E8AID2\/ref=sr_1_1?ie=UTF8&qid=1483648485&sr=8-1&keywords=practical+formal+methods+using+temporal+logic"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-41540-6_1","volume-title":"Computer Aided Verification","author":"M Gario","year":"2016","unstructured":"Gario, M., Cimatti, A., Mattarei, C., Tonetta, S., Rozier, K.Y.: Model checking at scale: automated air traffic control design space exploration. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 3\u201322. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_1"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-319-11164-3_18","volume-title":"Runtime Verification","author":"J Geist","year":"2014","unstructured":"Geist, J., Rozier, K.Y., Schumann, J.: Runtime observer pairs and bayesian network reasoners on-board FPGAs: flight-certifiable system health management for embedded systems. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 215\u2013230. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_18"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Guarro, S., et al.: Formal framework and models for validation and verification of software-intensive aerospace systems. In: AIAA Information Systems-AIAA Infotech@ Aerospace, p. 0418 (2017)","DOI":"10.2514\/6.2017-0418"},{"key":"8_CR17","unstructured":"Kochenderfer, M.J., Chryssanthacopoulos, J.: Robust airborne collision avoidance through dynamic programming. Massachusetts Institute of Technology, Lincoln Laboratory, Project Report ATC-371 (2011)"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Mattarei, C., Cimatti, A., Gario, M., Tonetta, S., Rozier, K.Y.: Comparing different functional allocations in automated air traffic control design. In: Proceedings of Formal Methods in Computer-Aided Design (FMCAD 2015), Austin, Texas, USA. IEEE\/ACM, September 2015","DOI":"10.1109\/FMCAD.2015.7542260"},{"key":"8_CR19","unstructured":"Radio Technical Commission for Aeronautics: DO-333 \u2013 formal methods supplement to DO-178C and DO-278A (2011). https:\/\/www.rtca.org\/content\/standards-guidance-materials"},{"key":"8_CR20","unstructured":"Radio Technical Commission for Aeronautics: DO-178C\/ED-12C \u2013 software considerations in airborne systems and equipment certification (2012). https:\/\/www.rtca.org\/content\/standards-guidance-materials"},{"key":"8_CR21","unstructured":"Radio Technical Commission for Aeronautics (RTCA): DO-178B: Software considerations in airborne systems and equipment certification, December 1992"},{"key":"8_CR22","unstructured":"Radio Technical Commission for Aeronautics (RTCA): DO-254: Design assurance guidance for airborne electronic hardware, April 2000"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-642-54862-8_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Reinbacher","year":"2014","unstructured":"Reinbacher, T., Rozier, K.Y., Schumann, J.: Temporal-logic based runtime observer pairs for system health management of real-time systems. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 357\u2013372. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_24"},{"key":"8_CR24","unstructured":"Rozier, K.Y., Schumann, J., Ippolito, C.: Intelligent hardware-enabled sensor and software safety and health management for autonomous UAS. Technical Memorandum NASA\/TM-2015-218817, NASA, NASA Ames Research Center, Moffett Field, CA 94035, USA, May 2015"},{"issue":"2","key":"8_CR25","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/j.cosrev.2010.06.002","volume":"5","author":"K Rozier","year":"2011","unstructured":"Rozier, K.: Linear temporal logic symbolic model checking. Comput. Sci. Rev. J. 5(2), 163\u2013203 (2011). https:\/\/doi.org\/10.1016\/j.cosrev.2010.06.002","journal-title":"Comput. Sci. Rev. J."},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Rozier, K., Rozier, E.: Reproducibility, correctness, and buildability: the three principles for ethical public dissemination of computer science and engineering research. In: IEEE International Symposium on Ethics in Engineering, Science, and Technology, Ethics 2014, pp. 1\u201313. IEEE, May 2014","DOI":"10.1109\/ETHICS.2014.6893384"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-73370-6_11","volume-title":"Model Checking Software","author":"KY Rozier","year":"2007","unstructured":"Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 149\u2013167. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73370-6_11"},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/978-3-642-21437-0_31","volume-title":"FM 2011: Formal Methods","author":"KY Rozier","year":"2011","unstructured":"Rozier, K.Y., Vardi, M.Y.: A multi-encoding approach for LTL symbolic satisfiability checking. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 417\u2013431. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_31"},{"key":"8_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-39611-3_23","volume-title":"Hardware and Software: Verification and Testing","author":"KY Rozier","year":"2013","unstructured":"Rozier, K.Y., Vardi, M.Y.: Deterministic compilation of temporal safety properties in explicit state model checking. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 243\u2013259. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39611-3_23"},{"key":"8_CR30","unstructured":"NASA UTM Research Transition Team (RTT): NASA UTM NextGen concept of operations v1.0, May 2018. https:\/\/utm.arc.nasa.gov\/docs\/2018-UTM-ConOps-v1.0.pdf"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Rushby, J.: A safety-case approach for certifying adaptive systems. In: AIAA Infotech@ Aerospace Conference and AIAA Unmanned... Unlimited Conference, pp. 1\u201316 (2009)","DOI":"10.2514\/6.2009-1992"},{"key":"8_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-40793-2_1","volume-title":"Computer Safety, Reliability, and Security","author":"J Rushby","year":"2013","unstructured":"Rushby, J.: Logic and epistemology in safety cases. In: Bitsch, F., Guiochet, J., Ka\u00e2niche, M. (eds.) SAFECOMP 2013. LNCS, vol. 8153, pp. 1\u20137. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40793-2_1"},{"key":"8_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-319-23820-3_15","volume-title":"Runtime Verification","author":"J Schumann","year":"2015","unstructured":"Schumann, J., Moosbrugger, P., Rozier, K.Y.: R2U2: monitoring and diagnosis of security threats for unmanned aerial systems. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 233\u2013249. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23820-3_15"},{"key":"8_CR34","unstructured":"U.S. Department of Transportation Federal Aviation Administration: Introduction to TCAS II version 7.1, February 2011. hQ-111358. https:\/\/www.faa.gov\/documentlibrary\/media\/advisory_circular\/tcas%20ii%20v7.1%20intro%20booklet.pdf"},{"key":"8_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45319-9_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"MY Vardi","year":"2001","unstructured":"Vardi, M.Y.: Branching vs. linear time: final showdown. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 1\u201322. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45319-9_1"},{"key":"8_CR36","unstructured":"Wei, P., Atkins, E., Schnell, T., Rozier, K.Y., Hunter, G.: NSF PFI:BIC: pre-departure dynamic geofencing, en-route traffic alerting, emergency landing and contingency management for intelligent low-altitude airspace UAS traffic management, July 2017. https:\/\/www.nsf.gov\/awardsearch\/showAward?AWD_ID=1718420"},{"key":"8_CR37","unstructured":"Wiels, V., Delmas, R., Doose, D., Garoche, P.L., Cazin, J., Durrieu, G.: Formal verification of critical aerospace software. AerospaceLab (4), 1\u20138 (2012). https:\/\/hal.archives-ouvertes.fr\/hal-01184099"},{"key":"8_CR38","unstructured":"Zhao, Y., Rozier, K.Y.: Formal specification and verification of a coordination protocol for an automated air traffic control system. In: Proceedings of the 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012). Electronic Communications of the EASST, vol. 53. European Association of Software Science and Technology (2012)"},{"issue":"3","key":"8_CR39","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/j.scico.2014.04.002","volume":"96","author":"Y Zhao","year":"2014","unstructured":"Zhao, Y., Rozier, K.Y.: Formal specification and verification of a coordination protocol for an automated air traffic control system. Sci. Comput. Program. J. 96(3), 337\u2013353 (2014)","journal-title":"Sci. Comput. Program. J."},{"key":"8_CR40","doi-asserted-by":"crossref","unstructured":"Zhao, Y., Rozier, K.Y.: Probabilistic model checking for comparative analysis of automated air traffic control systems. In: Proceedings of the 33rd IEEE\/ACM International Conference On Computer-Aided Design (ICCAD 2014), San Jose, California, USA, pp. 690\u2013695. IEEE\/ACM, November 2014","DOI":"10.1109\/ICCAD.2014.7001427"}],"container-title":["Lecture Notes in Computer Science","Formal Methods Teaching"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-32441-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,29]],"date-time":"2022-09-29T07:21:27Z","timestamp":1664436087000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-32441-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030324407","9783030324414"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-32441-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"23 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FMTea","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Formal Methods Teaching Workshop","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tfm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/fmtea.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"14","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"64% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4,5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}