Infinite-state high-level MSCs: Model-checking and realizability

Message sequence charts (MSC) and High-level MSC (HMSC) is a visual notation for asynchronously communicating processes and a standard of the ITU. They usually represent incomplete specifications of required or forbidden properties of communication protocols. We consider in this paper two basic problems concerning the automated validation of HMSC specifications, namely model-checking and synthesis. We identify natural syntactic restrictions of HMSCs for which we can solve the above questions. We show first that model-checking for globally cooperative (and locally cooperative) HMSCs is decidable within the same complexity as for the restricted class of bounded HMSCs. Furthermore, model-checking local-choice HMSCs turns out to be as efficient as for finite-state (sequential) systems. The study of locally cooperative and local-choice HMSCs is motivated by the synthesis question, i.e., the question of implementing HMSCs through communicating finite-state machines (CFM) with additional message data. We show that locally cooperative and local-choice HMSCs are always implementable. Furthermore, the implementation of a local-choice HMSC is deadlock-free and of linear size.     

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.     

Analysis and verification of message sequence charts of distributed systems with the help of coloured Petri nets

The standard language of message sequence charts (MSCs) is designed to describe scenarios of object interaction. Due to their expressiveness and simplicity, MSC diagrams are widely used in practice at all stages of system design and development. In particular, the MSC language is used for describing communication behavior in distributed systems and communication protocols. In this paper, a method for analysis and verification of MSC and HMSC diagrams is considered. The method is based on translation of (H)MSCs into coloured Petri nets. The translation algorithms cover most standard elements of MSCs including data concepts. Size estimates of the CPN, which is the result of translation, are given. Properties of the resulting CPN are analyzed and verified by using the known system CPN Tools and the CPN verifier based on the known tool SPIN. The translation method is demonstrated with an example.     

Pattern Matching and Membership for Hierarchical Message Sequence Charts

Several formalisms and tools for software development use hierarchy in system design, for instance statecharts and diagrams in UML. Message sequence charts (MSCs) are a standardized notation for asynchronously communicating processes. The norm Z.120 also includes hierarchical HMSCs. Algorithms on MSCs rarely take into account all possibilities covered by the norm. In particular, hierarchy is not taken into account since the models that are usually considered are (flat) MSC-graphs, that correspond to the unfolding of hierarchical HMSCs. However, complexity can increase exponentially by unfolding. The aim of this paper is to show that basic algorithms can be designed such that they avoid the costly unfolding of hierarchical MSCs and HMSCs. We show this for the membership and the pattern matching problem. We prove that the membership problem for hierarchical HMSCs is PSPACE-complete. Then we describe a polynomial time algorithm for the pattern matching problem on hierarchical MSCs. The results were obtained while B. Genest was affiliated with LIAFA, Université Paris 7.     

Formal Techniques for Analysing Scenarios using Message Sequence Charts

This paper describes light-weight formal techniques based on Message Sequence Charts (MSCs) for capturing and validating early requirements and design. Our focus is on ease of use in specifying, simulating and validating scenarios, and checking their desired properties efficiently. We discuss how the formalism of High Level Message Sequence Charts (HMSCs or MSC'96), can be used to capture scenarios in use cases, thus enabling the use of tools for analysing them. We then present two formal semantics for HMSCs – an intuitive linear time semantics based on runs, and an operational semantics in terms of a labelled transition system. Next we present a way of describing desired properties of use case scenarios using templates, for validating scenarios with respect to informal requirements. The correctness properties of a collection of MSCs can then be established by efficient algorithms for finding paths in a directed graph representing the precedence relation on the events of the MSCs. We have implemented the operational semantics and the verification algorithms in the form of a simulation and verification tool for analysing scenarios.     

Testing protocols modeled as FSMs with timing parameters

An optimization method is introduced for generating minimum-length test sequences taking into account timing constraints for FSM models of communication protocols. Due to active timers in many of today's protocols, the number of consecutive self-loops that can be traversed in a given state before a timeout occurs is limited. A test sequence that does not consider timing constraints will likely be unrealizable in a test laboratory, thereby potentially resulting in the incorrect failing of valid implementations (or, vice versa). The solution uses a series of augmentations for a protocol's directed graph representation. The resulting test sequence is proven to be of minimum-length while not exceeding the tolerable limit of consecutive self-loops at each state. Although UIO sequences are used for state verification method, the results also are applicable to test generation that uses distinguishing or characterizing sequences.     

Modeling and analysis of value added services using message sequence charts

A value added service is an extension to the basic call/session establishment functionality of a network. Different teams develop services independently or in order to handle complexity, a service is often specified individually without any consideration to existing ones. These different services may behave correctly when they run separately, but may interact in a negative manner when they are integrated. This is known as service interaction. In this paper, we tackle the problem of service interaction detection in a formal setup. We use message sequence charts (MSC) to specify the behaviors of services as well as their properties. In our specification style, high-level MSC (HMSC) is used to describe the behavior of services from the user point of view, while basic MSCs (bMSCs) are used to describe these behaviors at an abstract network level. We describe service properties from a local point of view. The behavior of a service is first validated against its properties. For the detection of potential interactions between two services, instead of merging their behaviors and then check for the interactions, we first determine interaction-prone scenarios using known filtering techniques, then we verify whether the properties of one service are satisfied by the behavior of the other service without combining their behaviors. In the case of non-satisfaction, we conclude that an interaction has been detected.     

基于面向对象方法的ASN.1编解码的设计与实现

随着计算机和通信技术的发展，ASN．1作为多种协议在表示层的抽象语法记法，它的作用在多媒体通信，协议测试等领域都非常重要。该文采用面向对象的设计方法实现了ASN．1标准X690，同时，通过比较各种编码规则的特点，在BER编解码实现的基础上，给出CER、DER及PER编码的实现方案，据此实现的ASN．1编解码对外提供了一致的接口，具有很好的通用性。     

An Algorithm for Checking the Time Consistency of Message Sequence Charts

The problem of time consistency check of message sequence charts (MSCs) with time specification of events is considered. The analyzed subset of the MSC language includes means of messaging and synchronizing conditions. The necessary and sufficient criterion of the property of time consistency of MSCs and an algorithm for checking this property are given. A prototype of this algorithm is realized in the C++ language.     

Causal Message Sequence Charts

Scenario languages based on Message Sequence Charts (MSCs) have been widely studied in the last decade. The high expressive power of MSCs renders many basic problems concerning these languages undecidable. However, several of these problems are decidable for languages that possess a behavioral property called “existentially bounded”. Unfortunately, collections of scenarios outside this class are frequently exhibited by systems such as sliding window protocols. We propose here an extension of MSCs called causal Message Sequence Charts and a natural mechanism for defining languages of causal MSCs called causal HMSCs (CaHMSCs). These languages preserve decidable properties without requiring existential bounds. Further, they can model collections of scenarios generated by sliding window protocols. We establish here the basic theory of CaHMSCs as well as the expressive power and complexity of decision procedures for various subclasses of CaHMSCs. We also illustrate the modeling power of our formalism with the help of a realistic example based on the TCP sliding window feature.     

Restrictive partially blind signature for resource-constrained information systems

Restrictive partially blind signature, which is designed for privacy-oriented information systems, allows a user to obtain a blind signature from a signer while the blind message must obey some certain rules. In order to reduce storage and communication costs, several public-key cryptosystems are constructed using characteristic sequences generated by linear feedback shift register (LFSR). In this paper, we present a new partially blind signature scheme with the restrictive property, which is based on nth order characteristic sequences generated by LFSR. By assuming the intractability of the discrete logarithm problem, our sequence-based schemes are provably secure in the random oracle model. We also present a practical e-cash application based on our restrictive partially blind signature. Due to the reduced representation of finite field elements and feasible sequence operations from LFSR, our scheme is time- and storage-efficient on both of signer and user sides. The advantages will make privacy-oriented applications more practical for resource-constrained devices.     

基于协议逆向的移动终端通信数据解析

针对移动终端通信协议及通信数据的解析,其难点在于大部分移动终端应用程序并无相关公开的技术文档,难以获知其采取的通信协议类型。指令执行序列分析技术通过分析程序执行的指令序列逆向推断出消息格式和状态机。但有时序列信息采集不全,导致状态机推断不完备,从而无法获取全部协议信息。针对上述问题,提出了一个新型的基于状态机对比推断分析的移动终端通信协议解析方案,可用于取证场景提高数据取证的准确性和完备性。该方案首先利用PIN动态二进制插桩,识别污点源并跟踪污点轨迹分析出协议消息格式;然后根据格式信息对提取的协议消息进行聚类分析推断出原始状态机;最后利用最长公共子序列（LCS,longest common subsequence）算法与已知的协议状态机进行对比,相似度最高者即为推断出的通信协议类型。在Android平台上基于两类应用程序设计实验对该方案进行测试和评估,实验结果表明可准确提取应用程序的通信内容,实用价值强。     

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.     

Triggered Message Sequence Charts

This paper introduces triggered message sequence charts (TMSCs), a graphical, mathematically well-founded framework for capturing scenario-based system requirements of distributed systems. Like message sequence charts (MSCs), TMSCs are graphical depictions of scenarios, or exchanges of messages between processes in a distributed system. Unlike MSCs, however, TMSCs are equipped with a notion of trigger that permits requirements to be made conditional, a notion of partiality indicating that a scenario may be subsequently extended, and a notion of refinement for assessing whether or not a more detailed specification correctly elaborates on a less detailed one. The TMSC notation also includes a collection of composition operators allowing structure to be introduced into scenario specifications so that interactions among different scenarios may be studied. In the first part of this paper, TMSCs are introduced and their use in support of requirements modeling is illustrated via two extended examples. The second part develops the mathematical underpinnings of the language     

Algorithms for scheduling with applications to parallel computing

Scheduling of message passing for synchronous communication is found to be equivalent to colouring the edges of a graph without conflict. The graph edge-colouring problem, which has other applications, is studied. An algorithm which colours the graph with no more than deg + 1 colours, where deg is the degree of the graph, is implemented. The problem of minimising the sum of the largest weight for each colour is also investigated and an algorithm suggested. These algorithms are used to organise the communication as part of a finite element Euler solver. Different communication schemes and their effect on the performance of the flow solver are compared.     

A music notation construction engine for optical music recognition

Optical music recognition (OMR) systems are used to convert music scanned from paper into a format suitable for playing or editing on a computer. These systems generally have two phases: recognizing the graphical symbols (such as note‐heads and lines) and determining the musical meaning and relationships of the symbols (such as the pitch and rhythm of the notes). In this paper we explore the second phase and give a two‐step approach that admits an economical representation of the parsing rules for the system. The approach is flexible and allows the system to be extended to new notations with little effort—the current system can parse common music notation, Sacred Harp notation and plainsong. It is based on a string grammar and a customizable graph that specifies relationships between musical objects. We observe that this graph can be related to printing as well as recognizing music notation, bringing the opportunity for cross‐fertilization between the two areas of research. Copyright © 2003 John Wiley & Sons, Ltd.     

Specification and Verification using Message Sequence Charts

Message sequence charts is a notation used in practice by protocol designers and system engineers. In this survey, some of the recent results related to this notation, in the context of specification and automatic verification of communication protocols, are presented.