{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T04:17:09Z","timestamp":1749010629561,"version":"3.41.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319406473"},{"type":"electronic","value":"9783319406480"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-40648-0_15","type":"book-chapter","created":{"date-parts":[[2016,6,3]],"date-time":"2016-06-03T13:42:13Z","timestamp":1464961333000},"page":"191-205","source":"Crossref","is-referenced-by-count":4,"title":["Probabilistic Formal Verification of the SATS Concept of Operation"],"prefix":"10.1007","author":[{"given":"Muhammad Usama","family":"Sardar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nida","family":"Afaq","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Khaza Anuarul","family":"Hoque","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Taylor T.","family":"Johnson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,4]]},"reference":[{"key":"15_CR1","unstructured":"Instrument Procedures Handbook. U.S. Department of Transportation, Federal Aviation Administration (2015)"},{"key":"15_CR2","unstructured":"PRISM - Probabilistic Symbolic Model Checker (2016). http:\/\/www.prismmodelchecker.org"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Computer Aided Verification","author":"T Arons","year":"2001","unstructured":"Arons, T., Pnueli, A., Ruah, S., Xu, Y., Zuck, L.D.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 221\u2013234. Springer, Heidelberg (2001)"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Bai, C., Zhang, X.: Aircraft landing scheduling in the small aircraft transportation system. In: International Conference on Computational and Information Sciences, pp. 1019\u20131022. IEEE (2011)","DOI":"10.1109\/ICCIS.2011.65"},{"key":"15_CR5","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P., et al.: Principles of model checking, vol. 26202649. MIT Press, Cambridge (2008)"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Baxley, B., Williams, D., Consiglio, M., Adams, C., Abbott, T.: The small aircraft transportation system (SATS), higher volume operations (HVO) off-nominal operations. In: Aviation, Technology, Integration, and Operations Conference. American Institute of Aeronautics and Astronautics (2005)","DOI":"10.2514\/6.2005-7461"},{"issue":"6","key":"15_CR7","doi-asserted-by":"crossref","first-page":"1825","DOI":"10.2514\/1.20493","volume":"45","author":"B Baxley","year":"2008","unstructured":"Baxley, B., Williams, D., Consiglio, M., Adams, C., Abbott, T.: Small aircraft transportation system, higher volume operations concept and research summary. J. Aircr. 45(6), 1825\u20131834 (2008)","journal-title":"J. Aircr."},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Carre\u00f1o, V.: Concept for multiple operations at non-tower non-radar airports during instrument meteorological conditions. In: Digital Avionics Systems Conference, vol. 1, pp. 5.B.1\u20135.1-9. IEEE (2003)","DOI":"10.1109\/DASC.2003.1245855"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Carre\u00f1o, V., Mu\u00f1oz, C.: Safety verification of the small aircraft transportation system concept of operations. In: Aviation, Technology, Integration, and Operations Conference. American Institute of Aeronautics and Astronautics (2005)","DOI":"10.2514\/6.2005-7423"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Cheng, A., Niktab, H., Walston, M.: Timing analysis of small aircraft transportation system (SATS). In: Conference on Embedded and Real-Time Computing Systems and Applications, pp. 58\u201367. IEEE (2012)","DOI":"10.1109\/RTCSA.2012.46"},{"key":"15_CR11","volume-title":"Model Checking","author":"EM Clarke Jr","year":"1999","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Consiglio, M., Conway, S., Adams, C., Syed, H.: SATS HVO procedures for priority landings and mixed VFR\/IFR operations. In: Digital Avionics Systems Conference, vol. 2, pp. 13.B.2-1\u201313.B.2-8. IEEE (2005)","DOI":"10.1109\/DASC.2005.1563428"},{"key":"15_CR13","unstructured":"Dowek, G., Munoz, C., Carre\u00f1o, V.A.: Abstract model of the SATS concept of operations: Initial results and recommendations. Technical report NASA\/TM-2004-213006, NASA Langley Research Center (2004)"},{"issue":"4","key":"15_CR14","doi-asserted-by":"crossref","first-page":"528","DOI":"10.1109\/TC.2007.1012","volume":"56","author":"A Fedeli","year":"2007","unstructured":"Fedeli, A., Fummi, F., Pravadelli, G.: Properties incompleteness evaluation by functional verification. IEEE Trans. Comput. 56(4), 528\u2013544 (2007)","journal-title":"IEEE Trans. Comput."},{"key":"15_CR15","unstructured":"Gariel, M., Spieser, K., Frazzoli, E.: On the statistics and predictability of go-arounds. In: Conference on Intelligent Data Understanding (2011)"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Greco, A., Magyarits, S., Doucett, S.: Air traffic control studies of small aircraft transportation system operations. In: Digital Avionics Systems Conference, vol. 2, pp. 13.A.4-1\u201313.A.4-12. IEEE (2005)","DOI":"10.1109\/DASC.2005.1563425"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"G\u00fcdemann, M., Ortmeier, F.: A framework for qualitative and quantitative formal model-based safety analysis. In: Symposium on High-Assurance Systems Engineering, pp. 132\u2013141. IEEE (2010)","DOI":"10.1109\/HASE.2010.24"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Hoque, K.A., Mohamed, O.A., Savaria, Y.: Towards an accurate reliability, availability and maintainability analysis approach for satellite systems based on probabilistic model checking. In: Design, Automation Test in Europe Conference Exhibition, pp. 1635\u20131640. IEEE (2015)","DOI":"10.7873\/DATE.2015.0817"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Johnson, T.T., Mitra, S.: Parameterized verification of distributed cyber-physical systems: an aircraft landing protocol case study. In: International Conference on Cyber-Physical Systems, pp. 161\u2013170. IEEE (2012)","DOI":"10.1109\/ICCPS.2012.24"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1007\/978-3-642-30793-5_2","volume-title":"Formal Techniques for Distributed Systems","author":"TT Johnson","year":"2012","unstructured":"Johnson, T.T., Mitra, S.: A small model theorem for rectangular hybrid automata networks. In: Giese, H., Rosu, G. (eds.) FORTE 2012 and FMOODS 2012. LNCS, vol. 7273, pp. 18\u201334. Springer, Heidelberg (2012)"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Johnson, T.T., Mitra, S.: Invariant synthesis for verification of parameterized cyber-physical systems with applications to aerospace systems. In: Infotech at Aerospace Conference. American Institute of Aeronautics and Astronautics (2013)","DOI":"10.2514\/6.2013-4811"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"issue":"4","key":"15_CR23","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1145\/1013886.1007536","volume":"29","author":"C Mu\u00f1oz","year":"2004","unstructured":"Mu\u00f1oz, C., Dowek, G., Carre\u00f1o, V.: Modeling and verification of an air traffic concept of operations. Softw. Eng. Notes 29(4), 175\u2013182 (2004)","journal-title":"Softw. Eng. Notes"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1007\/11916246_16","volume-title":"Rigorous Development of Complex Fault-Tolerant Systems","author":"C Mu\u00f1oz","year":"2006","unstructured":"Mu\u00f1oz, C., Carre\u00f1o, V.A., Dowek, G.: Formal analysis of the operational concept for the small aircraft transportation system. In: Butler, M., Jones, C.B., Romanovsky, A., Troubitsyna, E. (eds.) Rigorous Development of Complex Fault-Tolerant Systems. LNCS, vol. 4157, pp. 306\u2013325. Springer, Heidelberg (2006)"},{"key":"15_CR25","unstructured":"Mu\u00f1oz, C., Dowek, G.: Hybrid verification of an air traffic operational concept. In: IEEE ISoLA Workshop on Leveraging Applications of Formal Methods, Verification, and Validation (2005)"},{"key":"15_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Peters, M.: Capacity analysis of the NASA Langley airport management module. In: Digital Avionics Systems Conference, vol. 1, pp. 4.D.6\u201341\u201312. IEEE (2005)","DOI":"10.1109\/DASC.2005.1563367"},{"key":"15_CR28","unstructured":"Sardar, M.U., Hoque, K.A.: Probabilistic formal verification of the SATS concept of operation (2016). http:\/\/save.seecs.nust.edu.pk\/projects\/SATS"},{"key":"15_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1007\/11813040_5","volume-title":"FM 2006: Formal Methods","author":"S Umeno","year":"2006","unstructured":"Umeno, S., Lynch, N.A.: Proving safety properties of an aircraft landing protocol using I\/O automata and the PVS theorem prover: a case study. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 64\u201380. Springer, Heidelberg (2006)"},{"key":"15_CR30","doi-asserted-by":"crossref","unstructured":"Viken, S.A., Brooks, F.M.: Demonstration of four operating capabilities to enable a small aircraft transportation system. In: Digital Avionics Systems Conference, vol. 2, pp. 13.A.1-1\u201313.A.1-16. IEEE (2005)","DOI":"10.1109\/DASC.2005.1563422"},{"key":"15_CR31","unstructured":"Williams, D.M.: Point-to-point! validation of the small aircraft transportation system higher volume operations concept. In: International Congress of Aeronautical Sciences (2006)"},{"key":"15_CR32","doi-asserted-by":"crossref","unstructured":"Williams, D., Consiglio, M., Murdoch, J., Adams, C.: Flight technical error analysis of the SATS higher volume operations simulation and flight experiments. In: Digital Avionics Systems Conference, vol. 2, pp. 13.B.1-1\u201313.B.1-12. IEEE (2005)","DOI":"10.1109\/DASC.2005.1563427"},{"key":"15_CR33","doi-asserted-by":"crossref","unstructured":"Xu, Y., Baik, H., Trani, A.: A preliminary assessment of airport noise and emission impacts induced by small aircraft transportation system operations. In: Aviation Technology, Integration and Operations Conference. American Institute of Aeronautics and Astronautics (2006)","DOI":"10.2514\/6.2006-7736"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40648-0_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T20:35:15Z","timestamp":1748982915000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40648-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319406473","9783319406480"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40648-0_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}