Ordering Strict Partial Orders to Model Behavioral Refinement

TL;DR

This paper introduces a formal order relation between strict partial orders to verify temporal refinement in asynchronous systems, aiding the development of complex cyber-physical systems with precise time management.

Contribution

It defines a novel formal construct for verifying time refinement in asynchronous systems using strict partial orders, implemented in Agda.

Findings

Formal order relation enables distinguishing coincident events at different abstraction levels.

The approach preserves abstract properties during refinement.

Implemented and verified using the Agda proof assistant.

Abstract

Software is now ubiquitous and involved in complex interactions with the human users and the physical world in so-called cyber-physical systems where the management of time is a major issue. Separation of concerns is a key asset in the development of these ever more complex systems. Two different kinds of separation exist: a first one corresponds to the different steps in a development leading from the abstract requirements to the system implementation and is qualified as vertical. It matches the commonly used notion of refinement. A second one corresponds to the various components in the system architecture at a given level of refinement and is called horizontal. Refinement has been studied thoroughly for the data, functional and concurrency concerns while our work focuses on the time modeling concern. This contribution aims at providing a formal construct for the verification of refinement in time models, through the definition of an order between strict partial orders used to relate the different instants in asynchronous systems. This relation allows the designer at the concrete level to distinguish events that are coincident at the abstract level while preserving the properties assessed at the abstract level. This work has been conducted using the proof assistant Agda and is connected to a previous work on the asynchronous language CCSL, which has also been modelled using the same tool.