Abstract
Advancement of AI-enhanced control in autonomous systems stands on the shoulders of formal methods, which make possible the rigorous safety analysis autonomous systems require. An aircraft cannot operate autonomously unless it has design-time reasoning to ensure correct operation of the autopilot and runtime reasoning to ensure system health management, or the ability to detect and respond to off-nominal situations. Formal methods are highly dependent on the specifications over which they reason; there is no escaping the “garbage in, garbage out” reality. Specification is difficult, unglamorous, and arguably the biggest bottleneck facing verification and validation of aerospace, and other, autonomous systems.
This VSTTE invited talk and paper examines the outlook for the practice of formal specification, and highlights the on-going challenges of specification, from design-time to runtime system health management. We exemplify these challenges for specifications in Linear Temporal Logic (LTL) though the focus is not limited to that specification language. We pose challenge questions for specification that will shape both the future of formal methods, and our ability to more automatically verify and validate autonomous systems of greater variety and scale. We call for further research into LTL Genesis.
Thanks to NASA’s Autonomy Operating System (AOS) Project and NSF CAREER Award CNS-1552934 for supporting this work.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Note that the term functional patterns has been used in a different context: describing Requirements Specification Language (RSL) patterns for system state changes in response to external stimuli [2].
- 2.
References
Alur, R., Henzinger, T.A.: Real-time logics: complexity and expressiveness. In: LICS, pp. 390–401. IEEE (1990)
Backes, J.D., Whalen, M.W., Gacek, A., Komp, J.: On implementing real-time specification patterns using observers. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 19–33. Springer, Heidelberg (2016). doi:10.1007/978-3-319-40648-0_2
Badger, J., Rozier, K.Y. (eds.): NFM 2014. LNCS, vol. 8430. Springer, Heidelberg (2014)
Badger, J., Rozier, K.Y.: Panel: future directions of specifications for formal methods. In: Badger, J., Rozier, K.Y. (eds.) NFM. LNCS, vol. 8430, pp. XX-XXI. Springer, May 2014
Badger, J., Throop, D., Claunch, C.: Vared: verification and analysis of requirements and early designs. In: Requirements Engineering, pp. 325–326. IEEE (2014)
Barnat, J., Bauch, P., Beneš, N., Brim, L., Beran, J., Kratochvíla, T.: Analysing sanity of requirements for avionics systems. Formal Aspects Comput. 28(1), 45–63 (2016)
Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. Formal Methods Syst. Des. 18(2), 141–162 (2001)
Bloem, R., Cimatti, A., Greimel, K., Hofferek, G., Könighofer, R., Roveri, M., Schuppan, V., Seeber, R.: RATSY – a new requirements analysis tool with synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 425–429. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14295-6_37
Bohy, A., Bruyère, V., Filiot, E., Jin, N., Raskin, J.-F.: Acacia+, a tool for LTL synthesis. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 652–657. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31424-7_45
Castillos, K.C., Dadeau, F., Julliand, J., Kanso, B., Taha, S.: A compositional automata-based semantics for property patterns. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 316–330. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38613-8_22
Chockler, H., Kupferman, O., Kurshan, R.P., Vardi, M.Y.: A practical approach to coverage in model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 66–78. Springer, Heidelberg (2001). doi:10.1007/3-540-44585-4_7
Cimatti, A., Roveri, M., Schuppan, V., Tchaltsev, A.: Diagnostic information for realizability. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 52–67. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78163-9_9
Dallmeier, V., Knopp, N., Mallon, C., Hack, S., Zeller, A.: Generating test cases for specification mining. In: ISSTA, pp. 85–96. ACM (2010)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: FMSP, pp. 7–15. ACM (1998)
Fisman, D., Kupferman, O., Sheinvald-Faragy, S., Vardi, M.Y.: A framework for inherent vacuity. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol. 5394, pp. 7–22. Springer, Heidelberg (2009). doi:10.1007/978-3-642-01702-5_7
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–22. Springer, Heidelberg (2016). doi:10.1007/978-3-319-41540-6_1
Gario, M., Cimatti, A., Mattarei, C., Tonetta, S., Rozier, K.Y.: Model checking at scale: automated air traffic control design space exploration. Presentation: https://es-static.fbk.eu/projects/nasa-aac/download/CAV2016_presentation.pdf#21 (2016-07-22)
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–230. Springer, Heidelberg (2014). doi:10.1007/978-3-319-11164-3_18
Gheorghiu, M., Gurfinkel, A., Chechik, M.: VaqUoT: a tool for vacuity detection. In: Posters & Research Tools Track, FM 2006 (2006)
Ghosh, S., Shankar, N., Lincoln, P., Elenius, D., Li, W., Steiener, W.: Automatic Requirements Specification Extraction from Natural Language (ARSENAL). Technical report, DTIC Document (2014)
Gross, K.H., Fifarek, A.W., Hoffman, J.A.: Incremental formal methods based design approach demonstrated on a coupled tanks control system. In: HASE, pp. 181–188. IEEE (2016)
Gundy-Burlet, K.: Validation and verification of LADEE models and software. In: 51st AIAA Aerospace Sciences Meeting Including the New Horizons Forum and Aerospace Exposition (2013)
Gurfinkel, A., Chechik, M.: Robust vacuity for branching temporal logic. ACM Trans. Comput. Logic (TOCL) 13(1), 1 (2012)
Heitmeyer, C., Jeffords, R., Labaw, B.: Automated consistency checking of requirements specifications. ACM Trans. Softw. Eng. Methodol. 5(3), 231–261 (1996)
Hoffman, J.A.: Utilizing assume guarantee contracts to construct verifiable simulink model blocks. S5 (2015). http://mys5.org/Proceedings/2015/Day_1/2015-S5-Day1_1255_Hoffman.pdf
Hoffman, J.A.: V&V of Autonomy: UxV Challenge Problem (UCP). S5 (2016). http://mys5.org/Proceedings/2016/Day_3/2016-S5-Day3_0805_Hoffman.pdf
Jackson, C.: Face it: The engineering V is outdated (2014). https://www.linkedin.com/pulse/20140721140340-5687591-face-it-the-engineering-v-is-outdated
Jafer, S., Chhaya, B., Durak, U., Gerlach, T.: Formal scenario definition language for aviation: aircraft landing case study. In: AIAA MST (2016)
Könighofer, R., Hofferek, G., Bloem, R.: Debugging unrealizable specifications with model-based diagnosis. In: Barner, S., Harris, I., Kroening, D., Raz, O. (eds.) HVC 2010. LNCS, vol. 6504, pp. 29–45. Springer, Heidelberg (2011). doi:10.1007/978-3-642-19583-9_8
Kupferman, O.: Sanity checks in formal verification. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 37–51. Springer, Heidelberg (2006). doi:10.1007/11817949_3
Kupferman, O., Vardi, M.: Vacuity detection in temporal model checking. J. Softw. Tools Technol. Transf. (STTT) 4(2), 224–233 (2003)
Kurshan, R.: FormalCheck User’s Manual. Cadence Design, Inc. (1998)
Li, J., Zhang, L., Pu, G., Vardi, M.Y., He, J.: LTL satisfiability checking revisited. In: TIME, pp. 91–98. IEEE (2013)
Li, J., Zhu, S., Pu, G., Vardi, M.Y.: SAT-based explicit LTL reasoning. In: Piterman, N. (ed.) HVC 2015. LNCS, vol. 9434, pp. 209–224. Springer, Heidelberg (2015). doi:10.1007/978-3-319-26287-1_13
Li, W., Dworkin, L., Seshia, S.A.: Mining assumptions for synthesis. In: MEMOCODE, pp. 43–50. IEEE (2011)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer Science & Business Media, New York (2012)
Mattarei, C., Cimatti, A., Gario, M., Tonetta, S., Rozier, K.Y.: Comparing different functional allocations in automated air traffic control design. In: FMCAD. IEEE/ACM (2015)
Pike, L., Wegmann, N., Niller, S., Goodloe, A.: Copilot: monitoring embedded systems. Innov. Syst. Softw. Eng. 9(4), 235–255 (2013)
Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364–380. Springer, Heidelberg (2005). doi:10.1007/11609773_24
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179–190 (1989)
Reinbacher, T., Rozier, K.Y., Schumann, J.: Temporal-logic based runtime observer pairs for system health management of real-time systems. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 357–372. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_24
Rodriguez, M.A., Neubauer, P.: The graph traversal pattern. arXiv preprint arXiv:1004.1001 (2010)
Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 149–167. Springer, Heidelberg (2007). doi:10.1007/978-3-540-73370-6_11
Rozier, K., Vardi, M.: LTL satisfiability checking. Int. J. Softw. Tools Technol. Transf. (STTT) 12(2), 123–137 (2010)
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–431. Springer, Heidelberg (2011). doi:10.1007/978-3-642-21437-0_31
RTCA: DO-178B: Software Considerations in Airborne Systems and Equipment Certification (1992). http://www.rtca.org
RTCA: DO-254: Design assurance guidance for airborne electronic hardware, April 2000
RTCA: DO-178C/ED-12C: Software considerations in airborne systems and equipment certification (2012). http://www.rtca.org
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–249. Springer, Heidelberg (2015). doi:10.1007/978-3-319-23820-3_15
Schumann, J., Moosbrugger, P., Rozier, K.Y.: Runtime analysis with R2U2: a tool exhibition report. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 504–509. Springer, Heidelberg (2016). doi:10.1007/978-3-319-46982-9_35
Schumann, J., Rozier, K.Y., Reinbacher, T., Mengshoel, O.J., Mbaya, T., Ippolito, C.: Towards real-time, on-board, hardware-supported sensor and software health management for Unmanned Aerial Systems. IJPHM 6(1), 1–27 (2015)
Vardi, M.Y.: From verification to synthesis. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 2–2. Springer, Heidelberg (2008). doi:10.1007/978-3-540-87873-5_2
Whalen, M.W., Rayadurgam, S., Ghassabani, E., Murugesan, A., Sokolsky, O., Heimdahl, M.P., Lee, I.: Hierarchical multi-formalism proofs of cyber-physical systems. In: MEMOCODE, pp. 90–95. IEEE (2015)
Zeller, A.: Specifications for free. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 2–12. Springer, Heidelberg (2011). doi:10.1007/978-3-642-20398-5_2
Zhao, Y., Rozier, K.Y.: Formal specification and verification of a coordination protocol for an automated air traffic control system. In: AVoCS. Electronic Communications of the EASST, vol. 53 (2012)
Zhao, Y., Rozier, K.Y.: Formal specification and verification of a coordination protocol for an automated air traffic control system. SCP J. 96(3), 337–353 (2014)
Zhao, Y., Rozier, K.Y.: Probabilistic model checking for comparative analysis of automated air traffic control systems. In: ICCAD, pp. 690–695. IEEE/ACM (2014)
Acknowledgments
Thanks to the VSTTE chairs Sandrine Blazy, Marsha Chechik, and Temesghen Kahsai for inviting this paper, which is the expansion of an invited talk delivered July 18, 2016. Thanks to Julia Badger for instigating the framing of the specification bottleneck as a series of questions for our NFM2014 panel. Thanks to André Platzer for encouraging me to update and expand on these challenges; a shorter, preliminary version of this talk appeared at the NSF Workshop on “Cyber-Physical System (CPS) Verification & Validation Industrial Challenges & Foundations (I&F): CPS and AI Safety” in May, 2016. (http://www.ls.cs.cmu.edu/CPSVVIF-2016/index.html.) Thanks to Arie Gurfinkel, Eric Rozier, and Johann Schumann for technical discussions on earlier drafts of this paper. Information on our recent work can be found at: http://laboratory.temporallogic.org.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Rozier, K.Y. (2016). Specification: The Biggest Bottleneck in Formal Methods and Autonomy. In: Blazy, S., Chechik, M. (eds) Verified Software. Theories, Tools, and Experiments. VSTTE 2016. Lecture Notes in Computer Science(), vol 9971. Springer, Cham. https://doi.org/10.1007/978-3-319-48869-1_2
Download citation
DOI: https://doi.org/10.1007/978-3-319-48869-1_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-48868-4
Online ISBN: 978-3-319-48869-1
eBook Packages: Computer ScienceComputer Science (R0)