Narrow Results

We extend the classic work of R.J. Parikh on context-free languages with operators min and max on unary alphabet. The new theory is called CAN (Compositional Algebra of Numbers) and can be used to model software processes that can be concatenated, concurrently executed, and recursively invoked. We propose and analyze an algorithm which constructs the execution time sets of a CAN in semilinear form. Finally, we consider several interesting variations of CAN whose execution time sets can be constructed with algorithms.

A theory of representation of semiautomata by canonical words and equivalences was developed in [7]. That work was motivated by trace-assertion specifications of software modules, but its focus was entirely on the underlying mathematical model. In the present paper we extend that theory to automata with Moore and Mealy outputs, and show how to apply the extended theory to the specification of modules. In particular, we present a unified view of the trace-assertion methodology, as guided by our theory. We illustrate this approach, and some specific issues, using several nontrivial examples. We include a discussion of finite versus infinite modules, methods of error handling, some awkward features of the trace-assertion method, and a comparison to specifications by automata. While specifications by trace assertions and automata are equivalent in power, there are cases where one approach appears to be more natural than the other. We conclude that, for certain types of system modules, formal specification by automata, as opposed to informal state machines, is not only possible, but practical.

In this paper, we introduce an observation relation as an abstraction of point-to-point communication in distributed architectures. After showing how its semantics and syntax can be embedded within the UNITY approach, we state general observation properties. Finally, we consider the description and the validation of a distributed mutual exclusion algorithm. The relevant aspect of such a validation is the exclusive use of refinements and observations properties for the proof of these refinements.

Nowadays, power is a dominant factor that constrains highly integrated hardware-systems designs. The implied problems of high power density, causing chip overheating, or limited power source in modern Internet-of-Things devices are most commonly dealt with the use of the dynamic power management. This method enables to use power-reduction techniques, such as clock gating, power gating, or voltage and frequency scaling. Since the adoption of power management is quite difficult in modern complex systems, there are new approaches evolving intended to simplify power-constrained systems design. We have also proposed such an approach, utilizing the system level of design abstraction and increased automation in the design process. In this paper, the proposed hybrid verification approach is described that represents an integral part of the suggested design methodology. It consists of formal and informal techniques, enabling the verification process to begin at the very early specification stage of the system development. Our approach helps a designer to create correct and consistent power-management specification and verifies whether the specified power intent is preserved after design refinement. The continuous automated verification steps can quickly find errors at early design stages and thus reduce the amount of design re-spins, which speeds-up the overall development process.

ISO and IEC have jointly developed two Formal Description Techniques (FDTs) for specifying distributed real time systems such as computer/telecommunications protocols. These are Lotos and Estelle. In this paper, a formal method for automated transformation of a Lotos specification to an Estelle specification is presented. The method is applicable to various Lotos specification styles and to various communications protocols of ISO OSI layers.

Our method has applications in conformance testing of such systems and building common semantic model for the various FDTs. In this paper, we develop an algorithm for constructing a 'Data Oriented'-Restricted Behavior Tree T that represent both the control flow aspects and the data flow aspects of the system. Then, we develop an algorithm for constructing the Estelle specifications from T. A minimization rule is also developed to optimize the size of the Estelle specification by reducing both the number of states and the number of transitions.

In component-based systems, there are several obstacles to using Design by Contract (DbC), particularly with respect to third-party components. Contracts are particularly valuable when debugging or testing composite software structures that include third-party components. However, existing approaches have critical weaknesses. First, existing approaches typically require a component's source code to be available if you wish to strip (or re-insert) checks. Second, documentation of the contract is either distributed separately from the component or embedded in the component's source code. Third, enabling and disabling specific kinds of checks on separate components from independent vendors can be a significant challenge. This paper describes an approach to representing contracts for .NET components using attributes. This contract information can be retrieved from the compiled component's metadata and used for many purposes. The paper also describes nContract, a tool that automatically generates run-time checks from embedded contracts. Such run-time checks can be generated and added to a system without requiring source code access or recompilation. Further, when checks for a given component are excluded, they impose no run-time overhead. Finally, a highly expressive, fine-grained mechanism for controlling user preferences about which specific checks are enabled or disabled is presented.

Proof scores are documents of comprehensible plans to prove theorems. The proof score approach to systems analysis is a method in which proof scores are used to verify that systems enjoy properties (or analyze systems). In this paper, we describe a way to analyze electronic commerce protocols with the proof score approach, which has been developed and refined through several case studies conducted.

The specification-based testing can be employed to evaluate software functionalities without knowing program code. Decisions are the primary form of the pre- and post-conditions in formal specifications. This work expatiates on logic coverage criteria for specification-based testing at great length. It proposes and then expounds mask logic coverage criteria to solve the problems which existing determinant logic coverage criteria cannot solve. A feasible test case generation algorithm based on mask logic coverage criteria is developed. The test cases satisfying mask logic coverage criteria can detect those errors caused by the mask property of conditions. An experiment is conducted to compare MC/DC, RC/DC and two mask logic coverage criteria (RMCC and GMCC) on their test effectiveness and fault detection ability. It also elaborates on the constraint among conditions, how to decompose and compose a complicated decision, and the relationship among decisions. All these can respectively clarify the coupling problem among conditions, the multiple occurrences of a condition in a decision, and the location of a decision in a specification or program. Additionally, coverage criteria including full true decision coverage, full false decision coverage, all sub-decisions coverage, unique condition true coverage and unique condition false coverage are proposed. The test sets satisfying these criteria can detect respectively different types of errors. Finally, the hierarchical subsumption relation is established among these presented coverage criteria and some existing ones, and various applicable scenarios for different coverage criteria are suggested.

The Security policy of a software system is a set of actions that the system should or should not do in given conditions. These actions can be considered as critical properties in many applications which require high level of safety, such as the military, bank or stock software systems. Security policy must be specified clearly in software requirements and then be followed strictly and correctly in implementations. User permission policy is one of the most important aspects in software security policy. This paper proposes an approach for checking the conformance between user permissions of an implementation and their given specifications. In this approach, the source code of a program is represented at an abstraction level called Abstract Syntax Tree, which are then checked against specification of user permissions expressed using Role-Based Access Control (RBAC). A checking tool has been developed and verified using several common examples.

This paper proposes a novel strategy for formally analyzing functional requirements specification (FRS) and applies it to the Automatic Train Protection and Block (ATPB) system, which is proposed to reconstruct conventional rail lines in Japan. Based on the FRS in natural language, firstly, dynamic state transitions are extracted to express the operational mechanisms and determine the system parameters. A complete model of the ATPB system is then established using Unified Modeling Language (UML) to express the system structure graphically and explicitly. After achieving a common understanding, a VDM++ model is established formally to redescribe the original FRS of the ATPB system which is written in natural language (i.e. Japanese). Following that, in order to ensure internal consistency of the specification, proof obligations of the VDM++ model are discharged. Furthermore, a comprehensive testing is implemented to ensure that the FRS meets actual requirements. Finally, the system is simulated strictly in accordance with the formal specification. Without any runtime errors, collisions or derailments, the results of the simulation demonstrate the high quality and safety of the specification.

Context-aware and self adaptive systems have become very popular during the last decade. As these technologies are increasingly used in the development of critical applications, their behavior should be extensively analyzed. While formal methods provide a wide range of techniques for reasoning about software systems, addressing formally the requirements of context-aware adaptive systems in a consistent way remains a challenge. To this end, in this paper we present an algebraic framework for their formal specification using Observational Transition Systems (OTSs) specified in the CafeOBJ algebraic specification language. This approach permits the verification of the design of such systems, and can be an effective approach to obtaining verified context-aware software. We apply the proposed framework to the modeling of a context-aware adaptive traffic monitoring system and use theorem proving techniques to prove safety properties for that system.

Agile methods have provided significant contributions to Software Engineering. This work presents a new process for Software Requirements Specification, integrating Agile Properties and regulated environments, such as aviation, medical, nuclear and automotive, among others. The Software in Regulated Environments (SRE) involves plan-driven methods with needed documentation to ensure safety, reliability, security, and discipline. This paper proposes a balance between agile and plan-driven methods. We define a new process, which explores and investigates the usage of agile methods in SRE. The scope of this paper is Requirements Engineering, which is considered as a set of activities involved in the management, elicitation, documentation, and maintenance of requirements. The Adile Requirements Specification (ARES) process contains four methods, 13 activities, and some required artifacts to ensure compliance with the following six relevant Software Standards for regulated environments: RTCA DO-178C, IEC 62304:2015, ECSS-E-ST-40C, IEC 61508-3, ISO/IEC/IEEE 12207, and IAEA SSG-39. The process evaluation was performed using two experiments: a Cockpit Display System (CDS) and a Healthcare Information System (HIS). These experiments were measured with appropriate metrics to ensure improvements in Software Requirements Specification and traceability among artifacts. The experimental results revealed that the ARES process works better than the original Scrum for Software in Regulated Environments. The ARES process can also be integrated with traditional software life cycles (Waterfall, V, and Incremental and Iterative), when applied in the Requirements Engineering phase.

As software control of time-critical functions in embedded systems becomes more common, a means for the precise specification of their behavior and formal methods for analyzing system requirements become increasingly important. Modechart is a graphical specification language introduced to meet this need. The main focus of this paper is on methods and supporting tools for representing and reasoning about properties of time-critical systems specified in Modechart. The paper describes a verification methodology which takes advantage of the structuring inherent in a Modechart specification to determine whether a system specification satisfies the required properties. The paper also describes the implementation of a mechanical verifier, based on the proposed approach, which has been recently integrated as part of the Modechart Toolset prototype development environment from the Naval Research Lab [7].

This paper presents our reachability tree logic (RTL) and its integration with time Petri nets to specify and verify the temporal behavior of high assurance systems. The specification phase begins with a system modeling to model system requirements into a time Petri net N and construct a reachability tree RT of N. We then use RTL to specify the desired temporal behavior as formula F. The verification phase uses a model-checking algorithm to check whether RT can satisfy F, that is to find firing sequences to satisfy F. If F is not satisfied, we then modify N into N′ and obtain a RT′ of the modified N′. The modification (refinement) continues until the modified RT′ can satisfy F. In addition, we will demonstrate how to reduce the complexity of model-checking by using our RTL-based algorithm. We have implemented a specification and verification toolkit called NCUPN (National Central University Petri Nets toolkit) using Java. NCUPN is now available on the Internet via

The specification of communication behavior is fundamental in developing interoperable transactions. In particular, the temporal ordering of messages exchanged between different communicating agents must be declaratively specified and verified in order to guarantee consistency of data in the various component systems. This paper shows that by expressing communication constraints in propositional temporal logic, the tableau method can be applied to construct a dependency graph. If the specification is correct, this method guarantees that all possible execution paths satisfying the specification will be generated. The declarative specification and verification of communication constraints in interoperable transactions is demonstrated using the classic business trip. It is argued that the specification formalism provides an improvement over the Flexible Transaction Model.

We study the set of eventually always hitting points for symbolic dynamics with specification. The measure and Hausdorff dimension of such fractal set are obtained. Moreover, we establish the stronger metric results by introducing a new quantity $L_N(\omega )$ which describes the maximal length of string of zeros of the prefix among the first $N$ iterations of $\omega$ in symbolic space. The Hausdorff dimensions of the level sets for this quantity are also completely determined.

Component-based design paradigm is of paramount importance due to prolific growth in the complexity of modern-day systems. Since the components are developed primarily by multi-party vendors and often assembled to realize the overall system, it is an onus of the designer to certify both the functional and nonfunctional requirements of such systems. Several of the earlier works concentrated on formally analyzing the behavioral correctness, safety, security, reliability and robustness of such compositional systems. However, the assurance for quality measures of such systems is also considered as an important parameter for their acceptance. Formalization of quality measures is still at an immature state and often dictated by the user satisfaction. This paper presents a novel compositional framework for reliable quality analysis of component-based systems from the formal quality specifications of its constituent components. The proposed framework enables elegant and generic computation methods for quality attributes of various component-based system structures. In addition to this, we provide a formal query-driven quality assessment and design exploration framework which enables the designer to explore various component structures and operating setups and finally converge into better acceptable systems. A detailed case-study is presented over a component-based system structure to show the efficacy and practicality of our proposed framework.

Like any other large and complex software systems, Service-Based Systems (SBSs) must evolve to fit new user requirements and execution contexts. The changes resulting from the evolution of SBSs may degrade their design and quality of service (QoS) and may often cause the appearance of common poor solutions in their architecture, called antipatterns, in opposition to design patterns, which are good solutions to recurring problems. Antipatterns resulting from these changes may hinder the future maintenance and evolution of SBSs. The detection of antipatterns is thus crucial to assess the design and QoS of SBSs and facilitate their maintenance and evolution. However, methods and techniques for the detection of antipatterns in SBSs are still in their infancy despite their importance. In this paper, we introduce a novel and innovative approach supported by a framework for specifying and detecting antipatterns in SBSs. Using our approach, we specify 10 well-known and common antipatterns, including Multi Service and Tiny Service, and automatically generate their detection algorithms. We apply and validate the detection algorithms in terms of precision and recall two systems developed independently, (1) Home-Automation, an SBS with 13 services, and (2) FraSCAti, an open-source implementation of the Service Component Architecture (SCA) standard with more than 100 services. This validation demonstrates that our approach enables the specification and detection of Service Oriented Architecture (SOA) antipatterns with an average precision of 90% and recall of 97.5%.

Current Requirement Engineering research must face the need to deal with the increasing scale of today's requirement specifications. One important and recent research direction is handling the consistency assurance between large scale specifications and many additional regulations (e.g. national and international norms and standards), which the specifications must consider or satisfy. For example, the specification volume for a single electronic control unit (ECU) in the automotive domain sums up to 3000 to 5000 pages distributed over 30 to 300 individual documents (specification and regulations).

In this work, we present an approach to automatically classify the requirements in a set of specification documents and regulations to content topics in order to improve review activities in identifying cross-document inconsistencies. An essential success criteria for this approach from an industrial perspective is a sufficient classification quality with minimal manual effort.

In this paper, we show the results of an evaluation in the domain of automotive specifications at Mercedes-Benz passenger cars. The results show that one manually classified specification is sufficient to derive automatic classifications for other documents within this domain with satisfactory recall and precision. So, the approach of using content topics is not only effective but also efficient in large scale industrial environments.

Multi-agent systems for a certain application area can be modeled at multiple levels of abstraction. Interlevel relations are a means to relate models from different abstraction levels. Three dimensions of abstraction often occurring are the process abstraction, temporal abstraction, and agent cluster abstraction dimension. In this paper a unifying formalization is presented that can be used as a framework to specify interlevel relations for any of such dimensions. The approach is illustrated by showing how a variety of different types of abstraction relations between multi-agent system models can be formally specified in a unified manner.