Journals Proceedings

Abstract

Given the architecture of a Cyber Physical System (CPS) in AADL (Architecture Analysis and Design Language), we aim to use a model based development approach for system construction. We use the Event-B formalism for modelling and analysis. The model decomposition mechanism in Event-B helps us in establishing a one to one correspondence between the AADL components and the Event-B sub-models. Using the example of an Adaptive Cruise Controller, we show how interesting architectural properties could be verified within the Event-B modelling framework.