Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems

Crystal Chang Din, Olaf Owe, Richard Bubel

2014

Abstract

We investigate the usage of a history-based specification approach for concurrent and distributed systems. In particular, we compare two approaches on checking that those systems behave according to their specification. Concretely, we apply runtime assertion checking and static deductive verification on two small case studies to detect specification violations, respectively to ensure that the system follows its specifications. We evaluate and compare both approaches with respect to their scope and ease of application. We give recommendations on which approach is suitable for which purpose as well as the implied costs and benefits of each approach.

Paper Citation

in Harvard Style

Chang Din C., Owe O. and Bubel R. (2014). Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems . In Proceedings of the 2nd International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD, ISBN 978-989-758-007-9, pages 480-487. DOI: 10.5220/0004877804800487

in Bibtex Style

@conference{modelsward14,
author={Crystal Chang Din and Olaf Owe and Richard Bubel},
title={Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems},
booktitle={Proceedings of the 2nd International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD,},
year={2014},
pages={480-487},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0004877804800487},
isbn={978-989-758-007-9},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 2nd International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD,
TI - Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems
SN - 978-989-758-007-9
AU - Chang Din C.
AU - Owe O.
AU - Bubel R.
PY - 2014
SP - 480
EP - 487
DO - 10.5220/0004877804800487