Using Agent JPF to Build Models for Other Model Checkers
Pages 273 - 289
Abstract
We describe an extension to the AJPF agent program model-checker so that it may be used to generate models for input into other, non-agent, model-checkers. We motivate this adaptation, arguing that it improves the efficiency of the model-checking process and provides access to richer property specification languages.
We illustrate the approach by describing the export of AJPF program models to Spin and Prism. In the case of Spin we also investigate, experimentally, the effect the process has on the overall efficiency of model-checking.
References
[1]
Dennis, L.A., Fisher, M., Webster, M., Bordini, R.H.: Model Checking Agent Programming Languages. Automated Software Engineering 191, 5---63 2012
[2]
Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model Checking Programs. Automated Software Engineering 102, 203---232 2003
[3]
Hunter, J., Raimondi, F., Rungta, N., Stocker, R.: A Synergistic and Extensible Framework for Multi-Agent System Verification. In: Ito, T., Jonker, C., Gini, M., Shehory, O. eds. Proc. 13th International Conference on Autonomous Agents and Multiagent Systems AAMAS. IFAAMAS 2013
[4]
Wooldridge, M.: Reasoning about Rational Agents. The MIT Press 2000
[5]
Emerson, E.A.: Temporal and Modal Logic. In: van Leeuwen, J. ed. Handbook of Theoretical Computer Science, pp. 996---1072. Elsevier 1990
[6]
Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Proc. 15th IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification XV, pp. 3---18. Chapman & Hall, Ltd., London 1996
[7]
Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory-efficient Algorithms for the Verification of Temporal Properties. In: Formal Methods in System Design, pp. 275---288 1992
[8]
Webster, M., Fisher, M., Cameron, N., Jump, M.: Formal Methods for the Certification of Autonomous Unmanned Aircraft Systems. In: Flammini, F., Bologna, S., Vittorini, V. eds. SAFECOMP 2011. LNCS, vol. 6894, pp. 228---242. Springer, Heidelberg 2011
[9]
Webster, M., Cameron, N., Jump, M., Fisher, M.: Generating Certification Evidence for Autonomous Unmanned Aircraft Using Model Checking and Simulation. Journal of Aerospace Computing, Information, and Communication 2013
[10]
Holzmann, G.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley 2004
[11]
Hindriks, K.V., de Boer, F.S., van der Hoek, W., Meyer, J.-J.C.: Agent Programming with Declarative Goals. In: Castelfranchi, C., Lespérance, Y. eds. ATAL 2000. LNCS LNAI, vol. 1986, pp. 228---243. Springer, Heidelberg 2001
[12]
Havelund, K., Lowry, M., Park, S., Pecheur, C., Penix, J., Visser, W., White, J.L.: Formal Analysis of the Remote Agent Before and After Flight. In: Proc. 5th NASA Langley Formal Methods Workshop, Virginia, USA 2000
[13]
Kars, P.: The Application of Promela and Spin in the BOS Project Abstract 1996, http://spinroot.com/spin/Workshops/ws96/Ka.pdf accessed May 30, 2013
[14]
Kirsch, M.T., Regenie, V.A., Aguilar, M.L., Gonzalez, O., Bay, M., Davis, M.L., Null, C.H., Scully, R.C., Kichak, R.A.: Technical Support to the National Highway Traffic Safety Administration NHTSA on the Reported Toyota Motor Corporation TMC Unintended Acceleration UA Investigation. NASA Engineering and Safety Center Technical Assessment Report January 2011
[15]
Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic Symbolic Model Checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. eds. TOOLS 2002. LNCS, vol. 2324, pp. 200---204. Springer, Heidelberg 2002
[16]
PRISM: Probabilistic Symbolic Model Checker, http://www.prismmodelchecker.org/ accessed May 31, 2013
[17]
Sierhuis, M., Clancey, W.J.: Modeling and Simulating Work Practice: A Method for Work Systems Design. IEEE Intelligent Systems 175, 32---41 2002
[18]
JPF' the Swiss Army Knife of JavaTM verification, http://babelfish.arc.nasa.gov/trac/jpf/ accessed June 9, 2013
[19]
Bordini, R.H., Fisher, M., Wooldridge, M., Visser, W.: Property-based slicing for agent verification. J. Log. and Comput. 196, 1385---1425 2009
[20]
Lincoln, N.K., Veres, S.M., Dennis, L.A., Fisher, M., Lisitsa, A.: Autonomous Asteroid Exploration - Agent Based Control for Autonomous Spacecraft in Complex Environments. IEEE Computational Intelligence Magazine, Special Issue on Computational Intelligence for Space Systems and Operations to appear
[21]
Dennis, L.A., Farwer, B.: Gwendolen: A BDI Language for Verifiable Agents. In: Proc. AISB Workshop on Logic and the Simulation of Interaction and Reasoning, AISB 2008
[22]
Babiak, T., Křetínský, M., ehák, V., Strejă ek, J.: LTL to Büchi Automata Translation: Fast and More Deterministic. In: Flanagan, C., König, B. eds. TACAS 2012. LNCS, vol. 7214, pp. 95---109. Springer, Heidelberg 2012
[23]
Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. Formal Methods in System Design, 1---27 2012
[24]
Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: A model checker for the verification of multi-agent systems. In: Bouajjani, A., Maler, O. eds. CAV 2009. LNCS, vol. 5643, pp. 682---688. Springer, Heidelberg 2009
- Using Agent JPF to Build Models for Other Model Checkers
Recommendations
Certifying Model Checkers
CAV '01: Proceedings of the 13th International Conference on Computer Aided VerificationModel Checking is an algorithmic technique to determine whether a temporal property holds of a program. For linear time properties, a model checker produces a counterexample computation if the check fails. This computation acts as a "certificate" of ...
Analysis of Real-Time Systems with CTL Model Checkers
This paper presents a new method for model checking dense real-time systems. The dense real-time system is modeled by a timed automaton and the property is specified with the temporal logic TCTL. Specification of the TCTL property is reduced to CTL and ...
Testing with model checkers: a survey
About a decade after the initial proposal to use model checkers for the generation of test cases we take a look at the results in this field of research. Model checkers are formal verification tools, capable of providing counterexamples to violated ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
September 2013
390 pages
ISBN:9783642406232
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 16 September 2013
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 25 Nov 2024
Other Metrics
Citations
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in