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

Research output: Book/ReportReportAcademic

59 Downloads (Pure)


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.
Original languageEnglish
Place of PublicationEindhoven
PublisherTechnische Universiteit Eindhoven
Number of pages19
Publication statusPublished - 2011

Publication series

NameComputer science reports
ISSN (Print)0926-4515


Dive into the research topics of 'Investigating the effects of designing industrial control software using push and poll strategies'. Together they form a unique fingerprint.

Cite this