Skip directly to: content | search

ExCAPE: Expeditions in Computer Augmented Program Engineering

Consistency in Multi-View Modeling

PI: Tripakis (Berkeley)

Modeling all aspects of a complex system within a single model is a difficult, if not impossible, task. Multi-view modeling is a methodology where different aspects of the system are captured by different models, or views. A key question then is consistency: if different views of a system have some degree of overlap, how can we guarantee that they are consistent, i.e., that they do not contradict each other? In this work we formulate this and other basic problems in multi-view modeling within an abstract formal framework. We then instantiate this framework in a discrete, finitestate system setting, and study how some key verification and synthesis problems can be solved in that setting. A key synthesis problem is the synthesis of “witness” systems. Consistency of a set of views V1; V2; ... ; Vk, is defined as existence of a witness system S, from which each view Vi is derived by an abstraction function ai, so that Vi = ai(S). The consistency verification problem is to check, given a set of views, and corresponding abstraction functions, whether the views are consistent. The synthesis problem is to synthesize a witness system. This work paves the way towards a framework where different aspects of a system can be specified separately, by different views or models (e.g., a functional model, a performance model, an energy model) and the system is synthesized automatically from these view-models [PTQWBTVD13,RS14].



Papers:

ExCAPE: Expeditions in Computer Augmented Program Engineering NSF National Science Foundation Award CCF-1138996