Compositional Verification of Non-Blockingness with Prioritised Events. Issue 28 (2022)

• Record Type: Journal Article
• Authors: Tang, Yiheng; Moor, Thomas
• Is Part Of: IFAC-PapersOnLine. Volume 55:Issue 28(2022)
• Page Start: 236
• Page End: 243
• Publication Date: 2022
• Subjects: discrete-event systems -- compositional verification -- non-conflicting -- non-blocking -- event priorities -- modular systems; Automatic control -- Periodicals; 629.805
• DOI: 10.1016/j.ifacol.2022.10.348
• Languages: English
• ISSNs: 2405-8963

Abstract

Abstract: This paper addresses the verification of non-blockingness for modular discrete-event systems, i.e., discrete-event systems that are composed from component models. For such systems, the explicit construction of a monolithic representation turns out intractable for relevant applications, since such a construction in general is of exponential cost w.r.t. the number of components. One well established approach to circumvent the need for a monolithic representation for the verification task at hand is to alternate (a) the substitution of individual components by abstractions and (b) the composition of only a small number of strategically chosen components at a time. When successful, one ends up with a single moderately sized automaton which does not represent the overall behaviour in any detail but which does block if and only if the original modular system fails to be non-conflicting. This approach is referred to as compositional verification and originates from the field of process algebra with more recent adaptations to finite automata models. The main contribution of the present study is the development of a number of abstraction rules valid for compositional verification of non-conflictingness in the presence of global event priorities, i.e., where high priority events from one component possibly preempt events with lower priority of other components.