Towards formal verification of ToolBus scripts

W.J. Fokkink, P. Klint, B. Lisser, Y.S. Usenko

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

3 Citations (Scopus)

Abstract

ToolBus allows one to connect tools via a software bus. Programming is done using the scripting language Tscript, which is based on the process algebra ACP. Tscript was originally designed to enable formal verification, but this option has so far not been explored in any detail. We present a method for analyzing a Tscript by translating it to the process algebraic language mCRL2, and then applying model checking to verify behavioral properties.
Original languageEnglish
Title of host publicationAlgebraic Methodology and Software Technology (12th International Conference, AMAST 2008, Urbana IL, USA, July 28-31, 2008, Proceedings)
EditorsJ. Meseguer, G. Rosu
Place of PublicationBerlin
PublisherSpringer
Pages160-166
ISBN (Print)978-3-540-79979-5
DOIs
Publication statusPublished - 2008

Publication series

NameLecture Notes in Computer Science
Volume5140
ISSN (Print)0302-9743

Fingerprint

Algebra
Formal verification

Cite this

Fokkink, W. J., Klint, P., Lisser, B., & Usenko, Y. S. (2008). Towards formal verification of ToolBus scripts. In J. Meseguer, & G. Rosu (Eds.), Algebraic Methodology and Software Technology (12th International Conference, AMAST 2008, Urbana IL, USA, July 28-31, 2008, Proceedings) (pp. 160-166). (Lecture Notes in Computer Science; Vol. 5140). Berlin: Springer. https://doi.org/10.1007/978-3-540-79980-1_13
Fokkink, W.J. ; Klint, P. ; Lisser, B. ; Usenko, Y.S. / Towards formal verification of ToolBus scripts. Algebraic Methodology and Software Technology (12th International Conference, AMAST 2008, Urbana IL, USA, July 28-31, 2008, Proceedings). editor / J. Meseguer ; G. Rosu. Berlin : Springer, 2008. pp. 160-166 (Lecture Notes in Computer Science).
@inproceedings{55be6c7ba42644c9bd68d9a1071c3fcc,
title = "Towards formal verification of ToolBus scripts",
abstract = "ToolBus allows one to connect tools via a software bus. Programming is done using the scripting language Tscript, which is based on the process algebra ACP. Tscript was originally designed to enable formal verification, but this option has so far not been explored in any detail. We present a method for analyzing a Tscript by translating it to the process algebraic language mCRL2, and then applying model checking to verify behavioral properties.",
author = "W.J. Fokkink and P. Klint and B. Lisser and Y.S. Usenko",
year = "2008",
doi = "10.1007/978-3-540-79980-1_13",
language = "English",
isbn = "978-3-540-79979-5",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "160--166",
editor = "J. Meseguer and G. Rosu",
booktitle = "Algebraic Methodology and Software Technology (12th International Conference, AMAST 2008, Urbana IL, USA, July 28-31, 2008, Proceedings)",
address = "Germany",

}

Fokkink, WJ, Klint, P, Lisser, B & Usenko, YS 2008, Towards formal verification of ToolBus scripts. in J Meseguer & G Rosu (eds), Algebraic Methodology and Software Technology (12th International Conference, AMAST 2008, Urbana IL, USA, July 28-31, 2008, Proceedings). Lecture Notes in Computer Science, vol. 5140, Springer, Berlin, pp. 160-166. https://doi.org/10.1007/978-3-540-79980-1_13

Towards formal verification of ToolBus scripts. / Fokkink, W.J.; Klint, P.; Lisser, B.; Usenko, Y.S.

Algebraic Methodology and Software Technology (12th International Conference, AMAST 2008, Urbana IL, USA, July 28-31, 2008, Proceedings). ed. / J. Meseguer; G. Rosu. Berlin : Springer, 2008. p. 160-166 (Lecture Notes in Computer Science; Vol. 5140).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Towards formal verification of ToolBus scripts

AU - Fokkink, W.J.

AU - Klint, P.

AU - Lisser, B.

AU - Usenko, Y.S.

PY - 2008

Y1 - 2008

N2 - ToolBus allows one to connect tools via a software bus. Programming is done using the scripting language Tscript, which is based on the process algebra ACP. Tscript was originally designed to enable formal verification, but this option has so far not been explored in any detail. We present a method for analyzing a Tscript by translating it to the process algebraic language mCRL2, and then applying model checking to verify behavioral properties.

AB - ToolBus allows one to connect tools via a software bus. Programming is done using the scripting language Tscript, which is based on the process algebra ACP. Tscript was originally designed to enable formal verification, but this option has so far not been explored in any detail. We present a method for analyzing a Tscript by translating it to the process algebraic language mCRL2, and then applying model checking to verify behavioral properties.

U2 - 10.1007/978-3-540-79980-1_13

DO - 10.1007/978-3-540-79980-1_13

M3 - Conference contribution

SN - 978-3-540-79979-5

T3 - Lecture Notes in Computer Science

SP - 160

EP - 166

BT - Algebraic Methodology and Software Technology (12th International Conference, AMAST 2008, Urbana IL, USA, July 28-31, 2008, Proceedings)

A2 - Meseguer, J.

A2 - Rosu, G.

PB - Springer

CY - Berlin

ER -

Fokkink WJ, Klint P, Lisser B, Usenko YS. Towards formal verification of ToolBus scripts. In Meseguer J, Rosu G, editors, Algebraic Methodology and Software Technology (12th International Conference, AMAST 2008, Urbana IL, USA, July 28-31, 2008, Proceedings). Berlin: Springer. 2008. p. 160-166. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-540-79980-1_13