Timing analysis of scenario‐based specifications using linear programming

Scenario‐based specifications (SBSs), such as UML interaction models, offer an intuitive and visual way of describing design requirements, and are playing an increasingly important role in the design of software systems. This paper presents an approach to timing analysis of SBSs expressed by UML interaction models. The approach considers more general and expressive timing constraints in UML sequence diagrams (SDs), and gives a solution to the reachability analysis, constraint conformance analysis and bounded delay analysis problems, which reduces these problems into linear programs. With the synchronous interpretation of the SD compositions, the timing analysis algorithms in the approach form a decision procedure for a class of SBSs where any loop in any path is time‐independent of the other parts in the path. These algorithms are also a semi‐decision procedure for general SBSs with both the synchronous and asynchronous composition semantics. The approach also supports bounded timing analysis of SBSs, which investigates all the paths in the bound limit one by one, and performs the timing analysis for each finite path by linear programming. A tool prototype has been developed to support this approach. Copyright © 2010 John Wiley & Sons, Ltd.     

A Semantics for Timed MSC

Message Sequence Charts (MSC) is a graphical and textual specification language developed by ITU-T. It is widely used in telecommunication software engineering for specifying behavioral scenarios. Recently, the time concept has been introduced into MSC'2000. To support the specification and verification of real-time systems using timed MSC, we need to define its formal semantics. In this paper, we use timed lposet as a semantic model and give a formal semantics for timed MSC. We first define an event in a timed MSC as a timed lposet, then give a formal semantics for timed basic MSCs, timed MSCs with structures and high-level MSCs. In this paper, we also discuss some important issues related to timed MSC.     

Compositional message sequence charts

A message sequence chart (MSC) is a standard notation for describing the interaction between communicating objects. It is popular among the designers of communication protocols. MSCs enjoy both a visual and a textual representation. High-level MSCs (HMSCs) allow specifying infinite scenarios and different choices. Specifically, an HMSC consists of a graph, where each node is a finite MSC with matched send and receive events, and vice versa. In this paper we demonstrate a weakness of HMSCs, which disallows one to model certain interactions. We will show, by means of an example, that some simple finite state communication protocol cannot be represented using HMSCs. We then propose an extension to the MSC standard which allows HMSC nodes to include unmatched messages. The corresponding graph notation will be called HCMSC, which stands for high-level Compositional message sequence charts. With the extended framework, we provide an algorithm for automatically constructing an MSC representation for finite state asynchronous message passing protocols.     

Implied Scenario Detection in the Presence of Behaviour Constraints

Scenario-based specifications describe how independent components interact to provide system level behaviour. The specified system decomposition and system behaviour can give rise to implied scenarios, which are the result of specifying the global behaviour of a system that will be implemented component-wise. The existence of implied scenarios is an indication that further validation with stakeholders must be done. An implied scenario can be accepted or rejected by stakeholders indicating that the implied scenario is acceptable system behaviour or a situation that should be avoided. In consequence, implied scenarios can be used to iteratively drive requirement elicitation. However, in order to do so, we must be capable of detecting implied scenarios in the presence of rejected implied scenarios, in other words in the presence of behaviour constraints. The contribution of this paper is a technique for detecting implied scenarios in message sequence chart (MSC) specifications that can be used in conjunction with behaviour constraints. The technique is based on building a Coordinator component that forces system components to follow the same sequence of basic MSCs as they go through a high-level MSC. The result is a model that behaves as specified in the MSC but does not comply with the MSC architecture. The resulting model is not a proposed implementation, rather a precise model of specified behaviour that can be used in combination with constrained implementation models to detect further implied scenarios.     

LSCs: Breathing Life into Message Sequence Charts

While message sequence charts (MSCs) are widely used in industry to document the interworking of processes or objects, they are expressively weak, being based on the modest semantic notion of a partial ordering of events as defined, e.g., in the ITU standard. A highly expressive and rigorously defined MSC language is a must for serious, semantically meaningful tool support for use-cases and scenarios. It is also a prerequisite to addressing what we regard as one of the central problems in behavioral specification of systems: relating scenario-based inter-object specification to state-machine intra-object specification. This paper proposes an extension of MSCs, which we call live sequence charts (or LSCs), since our main extension deals with specifying liveness, i.e., things that must occur. In fact, LSCs allow the distinction between possible and necessary behavior both globally, on the level of an entire chart and locally, when specifying events, conditions and progress over time within a chart. This makes it possible to specify forbidden scenarios, for example, and enables naturally specified structuring constructs such as subcharts, branching and iteration.     

An empirical study of control logic specifications for programmable logic controllers

This paper presents an empirical study of control logic specifications used to document industrial control logic code in manufacturing applications. More than one hundred input/output related property specifications from ten different reusable function blocks were investigated. The main purpose of the study was to provide understanding of how the specifications are expressed by industrial practitioners, in order to develop new tools and methods for specifying control logic software, as well as for evaluating existing ones. In this paper, the studied specifications are used to evaluate linear temporal logic in general and the specification language ST-LTL, tailored for functions blocks, in particular. The study shows that most specifications are expressed as implications, that should always be fulfilled, between input and output conditions. Many of these implications are complex since the input and output conditions may be mixed and involve sequences, timer issues and non-boolean variables. Using ST-LTL it was possible to represent all implications of this study. The few non-implication specifications could be specified in ST-LTL as well after being altered to suit the specification language. The paper demonstrates some advantages of ST-LTL compared to standard linear temporal logic and discusses possible improvements such as support for automatic rewrite of complex specifications.     

The Control Layer in Open Mechanized Reasoning Systems: Annotations and Tactics

We are interested in developing a methodology for integrating mechanized reasoning systems such as Theorem Provers, Computer Algebra Systems, and Model Checkers. Our approach is to provide a framework for specifying mechanized reasoning systems and to use specifications as a starting point for integration. We build on the work presented by Giunchigliaet al. (1994) which introduces the notion of Open Mechanized Reasoning Systems (OMRS) as a specification framework for integrating reasoning systems. An OMRS specification consists of three components: the logic component, the control component, and the interaction component. In this paper we focus on the control level. We propose to specify the control component by first adding control knowledge to the data structures representing the logic by means of annotations and then by specifying proof strategies via tactics. To show the adequacy of the approach we present and discuss a structured specification of constraint contextual rewriting as a set of cooperating specialized reasoning modules.     

Bounded MSC communication

Message sequence charts (MSCs) and high-level message sequence charts (HMSCs) are popular formalisms for the specification of communication protocols between asynchronous processes. An important concept in this context is the size of the communication buffers used between processes. Since real systems impose limitations on the capacity (or speed) of communication links, we ask whether a given HMSC can be implemented with respect to a given buffer size imposed by the environment. We introduce four different measures for buffer sizes and investigate for each of these measures the complexity of deciding whether a given MSC (or HMSC, or nested MSC) satisfies a given bound on the buffer size. The complexity of these problems varies between the classes P, NP, and coNP.