Property preservation is investigated as an approach tomodular verification, leading to reduction of the property verificationtimefor formal models. For modelling purposes, formalisms withmulti-waysynchronisations are considered. For the modular verificationtechniqueto work, a specific type of synchronisation is required forwhich a necessary condition is identified. It is a requirement on thesemantics of theformalism, which is restricted to permit simultaneousexecution only of component moves that make reference to each other.
On Conditions for Modular Verification in Systems of Synchronising Components
2011
Abstract
Property preservation is investigated as an approach tomodular verification, leading to reduction of the property verificationtimefor formal models. For modelling purposes, formalisms withmulti-waysynchronisations are considered. For the modular verificationtechniqueto work, a specific type of synchronisation is required forwhich a necessary condition is identified. It is a requirement on thesemantics of theformalism, which is restricted to permit simultaneousexecution only of component moves that make reference to each other.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
