NASA Logo, National Aeronautics and Space Administration

Projects & Tools

System-Level Verification of Autonomous Systems

funded by NASA's Intelligent Systems Project

People

NASA Ames

Summer Interns / Academic Visitors

Related projects

Publications

  • Blundell, C., Giannakopoulou, D., and Pasareanu, C.S. "Assume-Guarantee Testing". 4th Workshop on Specification and Verification of Component-Based Systems (SAVCBS 05), associated with the 5th joint meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2005), September 2005.

  • Giannakopoulou, D., Pasareanu, C.S., and Barringer, H., "Component Verification with Automatically Generated Assumptions". Journal of Automated Software Engineering, Kluwer Academic Publishers.
  • Barringer, H., Giannakopoulou, D., and Pasareanu, C.S. "Proof Rules for Automated Compositional Verification through Learning". 2nd Workshop on Specification and Verification of Component-Based Systems, associated with the 4th joint meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2003).
  • Cobleigh, J.M., Giannakopoulou, D., and Pasareanu, C.S. "Learning Assumptions for Compositional Verification", in Proc. of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003). April 2003, Warsaw, Poland. Springer, LNCS.

LTL2Buchi: translating LTL formula to Bchi automata

LTL2Buchi is a tool that translates linear-time temporal logic (LTL) formulae into Bchi automata. It is a JAVA implementation of the algorithm described in:


LTL2Buchi is used by the JavaPathFinder (JPF) tool and the Labelled Transition Systems Analyser ( LTSA). The LTSA uses LTL2Buchi to perform "fluent" model checking as described in:

  • Giannakopoulou, D. and Magee, J. "Fluent Model Checking for Event-Based Systems", in Proc. of the 4th joint meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2003), September 2003, Helsinki, Finland.

Download

LTL2Buchi is available for download, as a component of the JavaPathfinder project at NASA Ames Research Center. JavaPathfinder is open source project that you may access here .

People

First Gov logo
NASA Logo - nasa.gov