This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L. and Schnoebelen, Ph. Systems and Software Verification: Model-Checking Techniques and Tools, Springer. 2001.
Bryant, R. E. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8), 1986.
Burch, J. R., Clarke, E. M., McMillan, K. L., Dill, D. L. and Hwang, J. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, June 1992.
Cimatti, A., Clarke, E., Giunchiglia, F. and Roveri, M. NuSMV: a new symbolic model verifier. In Proceedings of International Conference on Computer-Aided Verification, 1999.
Clancy, D., Larson, W., Pecheur, C., Engrand, P. and Goodrich, C. Autonomous Control of an In-Situ Propellant Production Plant. Technology 2009 Conference, Miami, November 1999.
Clarke, E. M., Grumberg, O. and Peled, D. Model Checking, MIT Press. 1999.
Dill, D. L., Drexler, A. J., Hu, A. J. and Yang, C. H. Protocol Verification as a Hardware Design Aid. In 1992 IEEE International Conference on Computer Design: VLSI in Computers and Processors, IEEE Computer Society, 1992, pp 522–525.
Engrand, P. Model checking autonomy models for a martian propellant production plan. In Proceedings of the AAAI Symposium on Model-Based Validation of Intelligence, March 2001.
Gross, A. R., Sridhar, K. R., Larson, W. E., Clancy, D. J., Pecheur, C. and Briggs, G. A. Information Technology and Control Needs for In-Situ Resource Utilization. In Proceedings of the 50th IAF Congress, Amsterdam, Holland, October 1999.
Khatib, L., Muscettola, N. and Havelund, K. Verification of plan models using UPPAAL. In Proceedings of First Goddard Workshop on Formal Approaches to Agent-Based Systems, (LNAI 1871), Springer-Verlag, April 2000.
Khatib, L., Muscettola, N. and Havelund, K. Mapping temporal planning constraints into timed automata. In Eighth International Symposium on Temporal Representation and Reasoning, TIME-01, IEEE Computer Society, June 2001.
Holzmann, G. J. The Model Checker SPIN. IEEE Transactions on Software Engineering, 23(5), May 1997.
Larsen, K. G., Pettersson, P. and Yi, W. UPPAAL in a Nutshell. In Springer International Journal of Software Tools for Technology Transfer 1(1+2), 1997.
Muscettola, N. HSTS: Integrating planning and scheduling. In Intelligent Scheduling, M. Fox and M. Zweben, editors. Morgan Kaufmann. 1994.
Muscettola, N., Nayak, P. P., Pell, B. and Williams, B. Remote Agent: To Boldly Go Where No AI System Has Gone Before. Artificial Intelligence, 103(1–2):5–48, August 1998.
Nayak, P. P. et al. Validating the DS1 Remote Agent Experiment. In Proceedings of the 5th International Symposium on Artificial Intelligence, Robotics and Automation in Space (iSAIRAS-99), ESTEC, Noordwijk, 1999.
Pell, B., Bernard, D. E., Chien, S. A., Gat, E., Muscettola, N., Nayak, P. P., Wagner, M. and Williams, B. C. An Autonomous Spacecraft Agent Prototype. Autonomous Robots, 5(1), March 1998.
Penix, J., Pecheur, C., Havelund, K. Using Model Checking to Validate AI Planner Domain Models. In Proceedings of the 23rd Annual Software Engineering Workshop, NASA Goddard, December 1998.
Simmons, R. G., Goodwin, R., Haigh, K. Z., Koenig, S., O’sullivan, J. and Veloso, M. M. Xavier: Experience with a layered robot architecture. Intelligence, 2001.
Simmons, R. and Pecheur, C. Automating Model Checking for Autonomous Systems. AAAI Spring Symposium on Real-Time Autonomous Systems, March 2000.
Williams, B. C. and Nayak, P. P. A Model-Based Approach to Reactive Self-Configuring Systems. In Proceedings of AAAI-96, 1996.
Yang, B., Simmons, R., Bryant, R. and O’Hallaron, D. Optimizing symbolic model checking for invariant-rich models. In Proceedings of International Conference on Computer-Aided Verification, 1999.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag London Limited
About this chapter
Cite this chapter
Pecheur, C., Simmons, R., Engrand, P. (2006). Formal Verification of Autonomy Models. In: Rouff, C.A., Hinchey, M., Rash, J., Truszkowski, W., Gordon-Spears, D. (eds) Agent Technology from a Formal Perspective. NASA Monographs in Systems and Software Engineering. Springer, London. https://doi.org/10.1007/1-84628-271-3_11
Download citation
DOI: https://doi.org/10.1007/1-84628-271-3_11
Publisher Name: Springer, London
Print ISBN: 978-1-85233-947-0
Online ISBN: 978-1-84628-271-3
eBook Packages: Computer ScienceComputer Science (R0)