TY - GEN
T1 - A formal interactive verification environment for the plan execution interchange language
AU - Rocha, Camilo
AU - Cadavid, Héctor
AU - Muñoz, César
AU - Siminiceanu, Radu
PY - 2012
Y1 - 2012
N2 - The Plan Execution Interchange Language (PLEXIL) is an open source synchronous language developed by NASA for commanding and monitoring autonomous systems. This paper reports the development of the PLEXIL's Formal Interactive Verification Environment (PLEXIL5), a graphical interface to the formal executable semantics of PLEXIL. Among its main features, PLEXIL5 provides model checking of plans with support for formula editing and visualization of counterexamples, interactive simulation of plans at different granularity levels, and random initialization of external environment variables. The formal verification capabilities of PLEXIL5 are illustrated by means of a human-automation interaction model.
AB - The Plan Execution Interchange Language (PLEXIL) is an open source synchronous language developed by NASA for commanding and monitoring autonomous systems. This paper reports the development of the PLEXIL's Formal Interactive Verification Environment (PLEXIL5), a graphical interface to the formal executable semantics of PLEXIL. Among its main features, PLEXIL5 provides model checking of plans with support for formula editing and visualization of counterexamples, interactive simulation of plans at different granularity levels, and random initialization of external environment variables. The formal verification capabilities of PLEXIL5 are illustrated by means of a human-automation interaction model.
UR - http://www.scopus.com/inward/record.url?scp=84864326044&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-30729-4_24
DO - 10.1007/978-3-642-30729-4_24
M3 - Conference contribution
AN - SCOPUS:84864326044
SN - 9783642307287
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 343
EP - 357
BT - Integrated Formal Methods - 9th International Conference, IFM 2012, Proceedings
T2 - 9th International Conference on Integrated Formal Methods, IFM 2012
Y2 - 18 June 2012 through 21 June 2012
ER -