Event-B is one of the most commonly used rigorous methods that has proven its value in many applications. To support the development of cyber-physical systems (CPS) continuous extensions to the method have already been proposed and extensions to supporting tools are under development. In this paper further extensions are proposed addressing the need to support asynchronous behaviour of autonomous components in CPS. This can be accomplished by multiple Event-B machines with a semantics defined by concurrent runs, which preserve the semantics of single Event-B machines. This makes only sense, if shared locations are supported as well. A third extension covers partial updates, by means of which conflicting updates to shared locations with bulk data values such as sets or relations that are predominant in Event-B are avoided.
展开▼
