Unwinding Forward Correctability

Abstract

A state-machine formulation is given for forward correctability in event systems, to provide a type of unwinding result for this information flow security property. We show also how regular expression notation provides an easy mechanical tool for verifying forward correctability for small systems, which is necessary for the effective presentation of examples and exercises.