English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

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

Ordering Strict Partial Orders to Model Behavioral Refinement