K: A Wide Spectrum Language for Modeling, Programming and Analysis

Klaus Havelund, Rahul Kumar, Chris Delp, Bradley Clement

2016

Abstract

The formal methods community has over the years proposed various formally founded specification languages based on predicate logic and set theory. At the same time the model-based engineering community has pro- posed less formally founded graphical formalisms such as UML and SysML. We report on an effort to formally ground SysML in a textual formal language, named K, supporting classes, multiple inheritance, predicate logic and set theory. K contains programming constructs, and can thus be considered as a wide-spectrum modeling and programming language. We further explain the translation of a subset of this textual language to the input language of the SMT-LIB standard, and the application of Z3 for analysis of the generated SMT-LIB formu- las. The entire effort is part of a larger effort to develop a general purpose SysML development framework for designing systems, in support of NASA’s proposed 2022 mission to Jupiter’s moon Europa.

Paper Citation

in Harvard Style

Havelund K., Kumar R., Delp C. and Clement B. (2016). K: A Wide Spectrum Language for Modeling, Programming and Analysis . In Proceedings of the 4th International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD, ISBN 978-989-758-168-7, pages 111-122. DOI: 10.5220/0005741401110122

in Bibtex Style

@conference{modelsward16,
author={Klaus Havelund and Rahul Kumar and Chris Delp and Bradley Clement},
title={K: A Wide Spectrum Language for Modeling, Programming and Analysis},
booktitle={Proceedings of the 4th International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD,},
year={2016},
pages={111-122},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0005741401110122},
isbn={978-989-758-168-7},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 4th International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD,
TI - K: A Wide Spectrum Language for Modeling, Programming and Analysis
SN - 978-989-758-168-7
AU - Havelund K.
AU - Kumar R.
AU - Delp C.
AU - Clement B.
PY - 2016
SP - 111
EP - 122
DO - 10.5220/0005741401110122