Modern enterprise information systems are built following the paradigm of service-orientation. This paradigm promotes workflow-based software composition, where complex business processes are realized by orchestrating different, heterogenous components. These workflow descriptions evolve continuously, to adapt to changes in the business goals or in the enterprise policies. Software verification of evolving systems is challenging mainstream methodologies and tools. Formal verification techniques often conflict with the time constraints imposed by change management practices for evolving systems. Since changes in these systems are often local to restricted parts, an incremental verification approach could be beneficial.
In this paper we focus on the probabilistic verification of reliability requirements of structured workflows. We propose a novel incremental technique based on a syntactic-semantic approach. Reliability analysis is driven by the syntactic structure (defined by an operator-precedence grammar) of the workflow and encoded as semantic attributes associated with the grammar. Incrementality is achieved by coupling the evaluation of semantic attributes with an incremental parsing technique. The approach has been implemented in a prototype tool; preliminary experimental evaluation confirms the theoretical speedup over a nonincremental approach.