Property Preservation and Composition with Guarantees: From ASSERT to CHESS

While the demand for high-integrity applications continues to rise, industrial developers seek cost effective development strategies that are capable of delivering the required guarantees. The very nature of high-integrity software systems make a-posteriori verification totally inapt to meet the time, cost and quality constraints that impend on developers. What is wanted instead is a development method that facilitates early verification and that devolves to proven automation as many of the error-prone development tasks as practically possible. Model-driven engineering (MDE) is an especially fit option to explore in that respect. In a recent European project very interesting results were obtained in the development and industrial evaluation of an MDE process centered on the joint principles of correctness by construction and property preservation. The proceedings of that project were so encouraging in fact that a continuation of it was instigated with a challenging broader scope.This paper provides an account of the approach taken in the original project with regard to property preservation and outlines the intent of its continuation.