A formal interactive verification environment for the plan execution interchange language

Camilo Rocha; Héctor Cadavid; César Muñoz; Radu Siminiceanu

doi:10.1007/978-3-642-30729-4_24

A formal interactive verification environment for the plan execution interchange language

Camilo Rocha
, Héctor Cadavid
, César Muñoz
, Radu Siminiceanu

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

8 Scopus citations

Abstract

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.

Original language	English
Title of host publication	Integrated Formal Methods - 9th International Conference, IFM 2012, Proceedings
Pages	343-357
Number of pages	15
DOIs	https://doi.org/10.1007/978-3-642-30729-4_24
State	Published - 2012
Externally published	Yes
Event	9th International Conference on Integrated Formal Methods, IFM 2012 - Pisa, Italy Duration: 18 Jun 2012 → 21 Jun 2012

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	7321 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	9th International Conference on Integrated Formal Methods, IFM 2012
Country/Territory	Italy
City	Pisa
Period	18/06/12 → 21/06/12

Access to Document

10.1007/978-3-642-30729-4_24

Cite this

Rocha, C., Cadavid, H., Muñoz, C., & Siminiceanu, R. (2012). A formal interactive verification environment for the plan execution interchange language. In Integrated Formal Methods - 9th International Conference, IFM 2012, Proceedings (pp. 343-357). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7321 LNCS). https://doi.org/10.1007/978-3-642-30729-4_24

Rocha, Camilo ; Cadavid, Héctor ; Muñoz, César et al. / A formal interactive verification environment for the plan execution interchange language. Integrated Formal Methods - 9th International Conference, IFM 2012, Proceedings. 2012. pp. 343-357 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{5551f08eb9ae4e9faee2a9d3136ff47f,

title = "A formal interactive verification environment for the plan execution interchange language",

abstract = "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.",

author = "Camilo Rocha and H{\'e}ctor Cadavid and C{\'e}sar Mu{\~n}oz and Radu Siminiceanu",

year = "2012",

doi = "10.1007/978-3-642-30729-4\_24",

language = "English",

isbn = "9783642307287",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "343--357",

booktitle = "Integrated Formal Methods - 9th International Conference, IFM 2012, Proceedings",

note = "9th International Conference on Integrated Formal Methods, IFM 2012 ; Conference date: 18-06-2012 Through 21-06-2012",

}

Rocha, C, Cadavid, H, Muñoz, C & Siminiceanu, R 2012, A formal interactive verification environment for the plan execution interchange language. in Integrated Formal Methods - 9th International Conference, IFM 2012, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7321 LNCS, pp. 343-357, 9th International Conference on Integrated Formal Methods, IFM 2012, Pisa, Italy, 18/06/12. https://doi.org/10.1007/978-3-642-30729-4_24

A formal interactive verification environment for the plan execution interchange language. / Rocha, Camilo; Cadavid, Héctor; Muñoz, César et al.
Integrated Formal Methods - 9th International Conference, IFM 2012, Proceedings. 2012. p. 343-357 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7321 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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 - https://www.scopus.com/pages/publications/84864326044

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 -

Rocha C, Cadavid H, Muñoz C, Siminiceanu R. A formal interactive verification environment for the plan execution interchange language. In Integrated Formal Methods - 9th International Conference, IFM 2012, Proceedings. 2012. p. 343-357. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-30729-4_24

A formal interactive verification environment for the plan execution interchange language

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this