Investigating the effects of designing industrial control software using push and poll strategies

J.F. Groote, A.A.H. Osaiweran, M.T.W. Schuts, J.H. Wesselius

Onderzoeksoutput: Boek/rapportRapportAcademic

42 Downloads (Pure)

Samenvatting

In this paper we apply a number of design guidelines for circumventing the state space explosion problem from [J.F. Groote, T.W.D.M. Kouters, and A.A.H. Osaiweran, Specification guidelines to avoid the state space explosion problem, 2011] to the design and formal verification of a real industrial case, namely a controller of a power distribution unit of X-ray machines developed at Philips Healthcare. Through this work we investigate whether these guidelines are effective in designing practical applications. We provide a number of alternative designs that mainly incorporate pushing and polling strategies, taking into account a number of these guidelines. Using the pushing strategy components notify one another when information becomes available while using polling components ask for information only when it is needed. We find that designs that use a pushing strategy and do not apply such guide-lines typically lead to the generation of substantially more states. All demonstrated designs formally refine a single predefined external specification that captures the desired external behavior of the system. Moreover, all designs are deadlock free and do not exhibit any illegal interactions. This confirms our hypothesis that the design guidelines are really effective in practical contexts.
Originele taal-2Engels
Plaats van productieEindhoven
UitgeverijTechnische Universiteit Eindhoven
Aantal pagina's19
StatusGepubliceerd - 2011

Publicatie series

NaamComputer science reports
Volume1116
ISSN van geprinte versie0926-4515

Vingerafdruk Duik in de onderzoeksthema's van 'Investigating the effects of designing industrial control software using push and poll strategies'. Samen vormen ze een unieke vingerafdruk.

  • Citeer dit

    Groote, J. F., Osaiweran, A. A. H., Schuts, M. T. W., & Wesselius, J. H. (2011). Investigating the effects of designing industrial control software using push and poll strategies. (Computer science reports; Vol. 1116). Technische Universiteit Eindhoven.