Proving the Properties of Communicating Imperfectly-Clocked Synchronous Systems

Autor:	Julien Bertrane
Rok vydání:	2006
Předmět:	Set (abstract data type) Theoretical computer science Reduced product Computer science Constraint domain Bounding overwatch Sound analysis Static analysis Abstract interpretation Algorithm Domain (software engineering)
Zdroj:	Static Analysis ISBN: 9783540377566 SAS
DOI:	10.1007/11823230_24
Popis:	Our work aims at certifying that all the executions of several collaborating synchronous systems in a realistic environment follow a given specification. In order to analyze the numerous executions that may happen while considering a set of synchronous systems whose clocks are non-perfect and that communicate through non-instantaneous channels, we define two new abstract domains. The Changes counting domain and the Integral bounding domain gap the imprecisions of the previously defined Constraint domain that occur because of these hardware imprecisions. We define a reduced product between these domains that allows a much more precise though sound analysis than the three analyses that may have been defined in each domain.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::c699de523864e9af93d1eb1a734f37b0 https://doi.org/10.1007/11823230_24 Zobrazit plný text záznamu