A component framework where port compatibility implies weak termination

D. Bera, K.M. Hee, van, M.P.W.J. Osch, van, J.M.E.M. Werf, van der

Research output: Book/ReportReportAcademic

4 Citations (Scopus)
90 Downloads (Pure)


The design and verification of an asynchronous communicating system can be very complex. In this paper we focus on weak termination: in each reachable state, the system has the option to eventually terminate. We present a component framework and construction method that guarantees weak termination. In the framework, communication between components is modeled by portnets, a special class of workflow nets. A basic component defines the orchestration of the portnets. For weak termination, the orchestration should accord to each of the portnets. A composite component is built from basic components that offer some service via a portnet. We provide sufficient conditions to guarantee weak termination for composite components. Furthermore, we present a refinement-based construction procedure to derive a weakly terminating composite from an architectural diagram of the system.
Original languageEnglish
Place of PublicationEindhoven
PublisherTechnische Universiteit Eindhoven
Number of pages26
Publication statusPublished - 2011

Publication series

NameComputer science reports
ISSN (Print)0926-4515


Dive into the research topics of 'A component framework where port compatibility implies weak termination'. Together they form a unique fingerprint.

Cite this