Formal verification of functional properties of a SCR-style software requirements specification using PVS

Industrial software companies developing safety-critical systems are required to use rigorous safety analysis techniques to demonstrate compliance to regulatory bodies. In this paper, we describe an approach to formal verification of functional properties of requirements for an embedded real-time software written in software cost reduction (SCR)-style language using PVS specification and verification system. Key contributions of the paper include development of an automated method of translating SCR-style requirements into PVS input language as well as identification of property templates often needed in verification. Using specification for a nuclear power plant system, currently in operation, we demonstrate how safety demonstration on requirements can be accomplished while taking advantage of assurance provided by formal methods.     

Fault tree construction of hybrid system requirements using qualitative formal method

When specifying requirements for software controlling hybrid systems and conducting safety analysis, engineers experience that requirements are often known only in qualitative terms and that existing fault tree analysis techniques provide little guidance on formulating and evaluating potential failure modes. In this paper, we propose Causal Requirements Safety Analysis (CRSA) as a technique to qualitatively evaluate causal relationship between software faults and physical hazards. This technique, extending qualitative formal method process and utilizing information captured in the state trajectory, provides specific guidelines on how to identify failure modes and relationship among them. Using a simplified electrical power system as an example, we describe step-by-step procedures of conducting CRSA. Our experience of applying CRSA to perform fault tree analysis on requirements for the Wolsong nuclear power plant shutdown system indicates that CRSA is an effective technique in assisting safety engineers.     

Editorial - Software language engineering

Software languages play an important role in software development. Software languages are the artificial languages that are used to describe software systems at various abstraction levels. They are applied to describe requirements and designs for software, definitions of software architectures, and implementations of software systems. A huge variety of different technological spaces exist to describe languages: programming languages, software modeling languages, data modeling languages, domain-specific languages, ontology language, and others.     

WebML modelling in UML

In recent years, we have witnessed how the Web Engineering community has started using the standard unified modelling language (UML) notation, techniques and supporting tools for modelling Web systems, which has led to the adaptation to UML of several existing modelling languages, notations and development processes. This interest for being MOF and UML-compliant arises from the increasing need to interoperate with other notations and tools, and to exchange data and models, thus facilitating reuse. WebML, like any other domain-specific language, allows one to express in a precise and natural way the concepts and mechanisms of its domain of reference. However, it cannot fully interoperate with other notations, nor be integrated with other model-based tools. As a solution to these requirements, a UML 2.0 profile for WebML which allows WebML models to be used in conjunction with other notations and modelling tools has been described. The paper also evaluates UML 2.0 as a platform for Web modelling and identifies some key requirements for making this version of the standard more usable.     

SMV model-based safety analysis of software requirements

Fault tree analysis (FTA) is one of the most frequently applied safety analysis techniques when developing safety-critical industrial systems such as software-based emergency shutdown systems of nuclear power plants and has been used for safety analysis of software requirements in the nuclear industry. However, the conventional method for safety analysis of software requirements has several problems in terms of correctness and efficiency; the fault tree generated from natural language specifications may contain flaws or errors while the manual work of safety verification is very labor-intensive and time-consuming. In this paper, we propose a new approach to resolve problems of the conventional method; we generate a fault tree from a symbolic model verifier (SMV) model, not from natural language specifications, and verify safety properties automatically, not manually, by a model checker SMV. To demonstrate the feasibility of this approach, we applied it to shutdown system 2 (SDS2) of Wolsong nuclear power plant (NPP). In spite of subtle ambiguities present in the approach, the results of this case study demonstrate its overall feasibility and effectiveness.     

Validation of web service compositions

Web services support software architectures that can evolve dynamically. In particular, in this paper the focus is on architectures where services are composed (orchestrated) through a workflow described in the business process execution language (BPEL). It is assumed that the resulting composite service refers to external services through assertions that specify their expected functional and non-functional properties. On the basis of these assertions, the composite service may be verified at design time by checking that it ensures certain relevant properties. Because of the dynamic nature of Web services and the multiple stakeholders involved in their provision, however, the external services may evolve dynamically, and even unexpectedly. They may become inconsistent with respect to the assertions against which the workflow was verified during development. As a consequence, validation of the composition must extend to run time. In this work, an assertion language, called assertion language for BPEL process interactions (ALBERT), is introduced; it can be used to specify both functional and non-functional properties. An environment which supports design-time verification of ALBERT assertions for BPEL workflows via model checking is also described. At run time, the assertions can be turned into checks that a software monitor performs on the composite system to verify that it continues to guarantee its required properties. A TeleAssistance application is provided as a running example to illustrate our validation framework.     

Systematic evaluation of fault trees using real-time model checker UPPAAL

Fault tree analysis, the most widely used safety analysis technique in industry, is often applied manually. Although techniques such as cutset analysis or probabilistic analysis can be applied on the fault tree to derive further insights, they are inadequate in locating flaws when failure modes in fault tree nodes are incorrectly identified or when causal relationships among failure modes are inaccurately specified. In this paper, we demonstrate that model checking technique is a powerful tool that can formally validate the accuracy of fault trees. We used a real-time model checker UPPAAL because the system we used as the case study, nuclear power emergency shutdown software named Wolsong SDS2, has real-time requirements. By translating functional requirements written in SCR-style tabular notation into timed automata, two types of properties were verified: (1) if failure mode described in a fault tree node is consistent with the system's behavioral model; and (2) whether or not a fault tree node has been accurately decomposed. A group of domain engineers with detailed technical knowledge of Wolsong SDS2 and safety analysis techniques developed fault tree used in the case study. However, model checking technique detected subtle ambiguities present in the fault tree.     

Performance-based standards: safety instrumented functions and safety integrity levels

This paper discusses two international performance-based standards, ANSI/ISA S84.01 and IEC d61508 and the requirements they place upon companies that rely on electrical, electronic and programmable electronic systems to perform safety functions. Performance-based regulations are also discussed and common safety elements between the standards and regulations are identified. Several risk analysis techniques that can be used to comply with the aforementioned requirements are discussed and a simple example is used to illustrate the use, advantages and disadvantages of the techniques. The evaluation of safety integrity level (SIL) of the Safety Instrumented System (SIS) in terms of the probability to fail to function is outside the scope of this paper.     

Plant and safety system model

The design and development of a digital computer-based safety system for a nuclear power plant is a complex process. The process of design and product development must result in a final product free of critical errors; operational safety of nuclear power plants must not be compromised. This paper focuses on the development of a safety system model to assist designers, developers, and regulators in establishing and evaluating requirements for a digital computer-based safety system. The model addresses hardware, software, and human elements for use in the requirements definition process. The purpose of the safety system model is to assist and serve as a guide to humans in the cognitive reasoning process of establishing requirements. The goals in the use of the model are to: (1) enhance the completeness of the requirements and (2) reduce the number of errors associated with the requirements definition phase of a project.     

Evaluating formal properties of feature diagram languages

Feature diagrams (FDs) are a family of popular modelling languages, mainly used for managing variability in software product lines. FDs were first introduced by Kang et al. as part of the feature-oriented domain analysis (FODA) method back in 1990. Since then, various extensions of FODA FDs were devised to compensate for purported ambiguity and lack of precision and expressiveness. Recently, the authors surveyed these notations and provided them with a generic formal syntax and semantics, called free feature diagrams (FFDs). The authors also started investigating the comparative semantics of FFD with respect to other recent formalisations of FD languages. Those results were targeted at improving the quality of FD languages and making the comparison between them more objective. The previous results are recalled in a self-contained, better illustrated and better motivated fashion. Most importantly, a general method is presented for comparative semantics of FDs grounded in Harel and Rumpe's guidelines for defining formal visual languages and in Krogstie et al.'s semiotic quality framework. This method being actually applicable to other visual languages, FDs are also used as a language (re)engineering exemplar throughout the paper.     

Using Scrum and unified modelling language to analyze and design an automatic course scheduling system

This research used a case study methodology to examine large-scale software projects accomplished despite ambiguous customer requirements. This study adopted Scrum as the agile software development method and used unified modelling language (UML) diagrams to enhance design implementation documents and improve the software development process. This study presented how the case company explored a Scrum-based automatic course scheduling system for elementary and secondary schools. Through interviews, the case company incorporated customers’ requirements by using the corresponding UML diagrams, which helped the project team document the software development process and design the functions to satisfy customer demand. Then, the proposed method was introduced to the automatic elementary and secondary school course scheduling system project undertaken by the case company, verifying the feasibility of the proposed method. A few problems arose in the proposed software development process, and remedies were discussed. Software companies could use these results as a reference when implementing a large-scale software project with ambiguous customer requirements.     

Chaste: using agile programming techniques to develop computational biology software

Cardiac modelling is the area of physiome modelling where the available simulation software is perhaps most mature, and it therefore provides an excellent starting point for considering the software requirements for the wider physiome community. In this paper, we will begin by introducing some of the most advanced existing software packages for simulating cardiac electrical activity. We consider the software development methods used in producing codes of this type, and discuss their use of numerical algorithms, relative computational efficiency, usability, robustness and extensibility. We then go on to describe a class of software development methodologies known as test-driven agile methods and argue that such methods are more suitable for scientific software development than the traditional academic approaches. A case study is a project of our own, Cancer, Heart and Soft Tissue Environment, which is a library of computational biology software that began as an experiment in the use of agile programming methods. We present our experiences with a review of our progress thus far, focusing on the advantages and disadvantages of this new approach compared with the development methods used in some existing packages. We conclude by considering whether the likely wider needs of the cardiac modelling community are currently being met and suggest that, in order to respond effectively to changing requirements, it is essential that these codes should be more malleable. Such codes will allow for reliable extensions to include both detailed mathematical models--of the heart and other organs--and more efficient numerical techniques that are currently being developed by many research groups worldwide.     

Analysis of fault tolerance and reliability in distributed real-time system architectures

Safety critical real-time systems are becoming ubiquitous in many areas of our everyday life. Failures of such systems potentially have catastrophic consequences on different scales, in the worst case even the loss of human life. Therefore, safety critical systems have to meet maximum fault tolerance and reliability requirements. As the design of such systems is far from being trivial, this article focuses on concepts to specifically support the early architectural design. In detail, a simulation based approach for the analysis of fault tolerance and reliability in distributed real-time system architectures is presented. With this approach, safety related features can be evaluated in the early development stages and thus prevent costly redesigns in later ones.     

Development of a safety critical software requirements verification method with combined CPN and PVS: a nuclear power plant protection system application

Safety-critical software systems such as certain nuclear instrumentation and control (NI&C) systems should be developed with thorough verification. This study presents a method of software requirement verification with a case study for a nuclear power plant (NPP) protection system. The verification introduces colored petri net (CPN) for system modeling and prototype verification system (PVS) for mathematical verification. In order to aid flow-through from modeling by CPN to mathematical proof by PVS, an information extractor from CPN models has been developed in this paper. In order to convert the extracted information to the PVS specification language, a translator has also been developed. This combined method has been applied to the functional requirements of the Wolsong NPP Shut Down System #2 (SDS2); logical properties of the requirements were verified. Through this research, guidelines and a tool support for the use of formal methods have been developed for application to NI&C software verification.     

Biocharts: a visual formalism for complex biological systems

We address one of the central issues in devising languages, methods and tools for the modelling and analysis of complex biological systems, that of linking high-level (e.g. intercellular) information with lower-level (e.g. intracellular) information. Adequate ways of dealing with this issue are crucial for understanding biological networks and pathways, which typically contain huge amounts of data that continue to grow as our knowledge and understanding of a system increases. Trying to comprehend such data using the standard methods currently in use is often virtually impossible. We propose a two-tier compound visual language, which we call Biocharts, that is geared towards building fully executable models of biological systems. One of the main goals of our approach is to enable biologists to actively participate in the computational modelling effort, in a natural way. The high-level part of our language is a version of statecharts, which have been shown to be extremely successful in software and systems engineering. The statecharts can be combined with any appropriately well-defined language (preferably a diagrammatic one) for specifying the low-level dynamics of the pathways and networks. We illustrate the language and our general modelling approach using the well-studied process of bacterial chemotaxis.     

Safety propensity index for signalized and unsignalized intersections: Exploration and assessment

The objective of this study is to develop a safety propensity index (SPI) for both signalized and unsignalized intersections. Through the use of a structural equation modelling (SEM) approach safety is quantified in terms of multiple endogenous variables and related to various dimensions of exogenous variables. The singular valued SPI allows for identification of relationships between variables and lends itself well to a comparative analysis between models. The data provided by the Highway Safety Information System (HSIS) for the California transportation network was utilized for analysis. In total 22,422 collisions at unsignalized intersections and 20,215 collisions at signalized intersections (occurring between 2006 and 2010) were considered in the final models. The main benefits of the approach and the subsequent development of an SPI are (1) the identification of pertinent variables that effect safety at both intersection types, (2) the identification of similarities and differences at both types of intersections through model comparison, and (3) the quantification of safety in the form of an index such that a ranking system can be developed. If further developed, the adopted methodology may assist in safety related decision making and policy analysis.     

Developing manufacturing ontologies for knowledge reuse in distributed manufacturing environment

The use of ontologies for knowledge sharing and distributed collaboration has been widely recognised in the knowledge modelling community, but the lack of a systematic and constructive methodology for developing manufacturing ontologies has impeded their wide usage for knowledge reuse in distributed manufacturing environments. This paper presents a constructive, two-level knowledge modelling approach to systematically develop manufacturing ontologies using both software engineering and Semantic Web paradigms. The UML/OCL (Unified Modeling Language/Object Constraint Language)-based object modelling is used first to serve as a graphical and structured basis for conceptual communication between domain experts and knowledge engineers. The OWL/SWRL (Web Ontology Language/Semantic Web Rule Language)-based ontology modelling then extends the UML/OCL-based object models with added semantics using a progressive, semantics-oriented knowledge acquisition method. An illustrative example for manufacturing ontology development in the manufacturing industry for producing electronic connectors is used to demonstrate the practicality of the proposed approach.