Early Verification of Software Behavior in a Time Interval Framework
Paulo Sérgio Muniz Silva · 2003
Verification of software behavior in early moments of the development process is not an easy task. Typically, software engineers draw diagrams to reason about the software functional behavior, for example, drawing Message Sequence Charts (MSCs). Not always does the intended behavior described by MSCs correspond to their actual behavior. To help the verification of the actual behavior of MSCs, this paper describes an interpretation of (basic) MSCs in a temporal framework that formally represents the qualitative, and possibly imprecise, temporal information conveyed in MSCs. The framework is an algebra of binary relations on time intervals, and provides rules of reasoning about the temporal information. The interpretation provides a polynomialtime solution to the verification problem and lays the foundations of a model checking tool.