Automated Computation of Decomposable Synchronization
James M. Purtilo, Elizabeth L. White · 1997
High assurance systems have various types of system requirements, most notably safety, real-time, reliability, security and availability. The primary goal oj high assurance system designers is to integrate various functions of the system while preserving the system consistency with the requirements. In this paper we show how automated synchronization based on receptive safety rules facilitates this integration. GenEx is a synchronization tool that computes the synchronization conditions n,ecessary for the system components to satisfy their receptive safety requirements, while preservin,g the real-time an,d liveness properties of the system. The complexify of con,current software systems limits the use of formal development and verification techn,iques in industrial applications. GenEx computes the synchronization conditions independently for each receptive safety rule, thus significantly reducing the complexity of the behauior analysis. We show how, usin,g GenEr synchronization, we designed a controller for a medium-sized industrial production, system with safety. liveness and real-time requirements.