Testing-based formal verification (TBFV) is proposed to reduce test cost and guarantee software reliability by ensuring the correctness of all traversed program paths. An ideal target is to generate adequate test cases to traverse all of its execution paths. However, it is a rather ambitious criterion that can hardly be satisfied due to the potentially great amount of test cases required. To address this problem, we propose a new criterion called Condition Sequence Coverage (CSC) to maintain a good balance between program correctness and the number of test cases. In this paper, we refine the TBFV method and introduce the theoretical foundations of CSC. We also integrate CSC with functional scenario form (FSF) to automatically generate test cases for the TBFV method. In addition, we develop the tool support for Java and validate its effectiveness and accuracy through experimental comparisons.

Obtaining sufficient high-quality labeled data remains a critical challenge for training deep neural networks (DNNs). Recently, a specification-based method has been proposed to systematically define object characteristics for automated data generation. However, this approach typically relies on abstract descriptions, resulting in a gap between specifications and executable data generation. To address this issue, this paper proposes a two-level formal specification approach. Specifically, we apply the first-level specification to describe object characteristics and the second-level specification to define parameters and values suitable for data generation. This paper focuses on discussing both levels of specifications to facilitate human comprehension and machine handling to reduce the gap mentioned above. The performance of this approach is demonstrated through a case study on traffic sign recognition.

In the era where Web3.0 values data security and privacy, adopting groundbreaking methods to enhance privacy in recommender systems is crucial. Recommender systems need to balance privacy and accuracy, while also having the ability to overcome cold start problems. The Differential Trust Mechanism (DTM) introduced in this paper is such an approach. The DTM provides a unique use of Gaussian distributions in modeling trust relationships within data, offering a novel way to balance recommendation accuracy with user privacy. This mechanism innovatively applies differential privacy principles, using Gaussian noise addition to protect individual user data from inference attacks, while maintaining the integrity and utility of the overall dataset. Unlike traditional anonymization techniques that often compromise data utility or vulnerability to reverse engineering, DTM provides a robust solution by dynamically adjusting privacy levels based on the trustworthiness of data requests. By combining DTM with existing mainstream recommendation algorithms, the prediction accuracy of MAE and RMSE increases by at least 6.60% and 2.69%, respectively. This dual benefit positions DTM as a significant advancement in secure data processing, especially relevant for online businesses and platforms where personalized recommendations are crucial yet privacy concerns are paramount.

Instruction reordering is an essential optimization technique used in both compilers and multi-core processors to enhance parallelism and resource utilization. Although the original intent of this technique is to benefit the program, some improper reordering can significantly impact the program correctness, which we call instruction reordering vulnerability (IRV). However, existing methods detect IRV by defining CPU instruction reordering rules to schedule execution paths while neglecting compiler reordering, and thus generate false positives that require manual filtering and resulting in inefficiency. To bridge this gap, in this paper, we propose the IRV detection method, , which analyzes IRV characteristics and extracts vulnerability patterns, integrating program dependency analysis for compiler reordering and memory model constraints for CPU reordering. Specifically, we use static analysis based on specific patterns to narrow the analysis scope, and adopt log-based dynamic analysis to confirm vulnerability by checking the log constraints. We built the IRV benchmark to compare IRHunter with five state-of-the-art tools (i.e., GENMC, Nidhugg, CBMC, SHB, BiRD). IRHunter detected all 19 errors, doubling the best model checking tools' performance, with half the false positive rate of leading data race detectors. It was 10× faster on small programs and outperformed data race detectors on large programs.

Neural networks are extensively employed in safety-critical systems. However, these critical systems incorporating neural networks continue to pose risks due to the presence of adversarial examples. Although the security of neural networks can be enhanced by verification, verifying neural networks is an NP-hard problem, making the application of verification algorithms to large-scale neural networks a challenging task. For this reason, we propose NNTBFV, a framework that utilizes the principles of Testing-Based Formal Verification (TBFV) to simplify neural networks and verify the simplified networks. Unlike conventional neural network pruning techniques, this approach is based on specifications, with the goal of deriving approximate execution paths under given preconditions. To mitigate the potential issue of unverifiable conditions due to overly broad preconditions, we also propose a precondition partition method. Empirical evidence shows that as the range of preconditions narrows, the size of the execution paths also reduces accordingly. The execution path generated by NNTBFV is still a neural network, so it can be verified by verification tools. In response to the results from the verification tool, we provide a theoretical method for analysis. We evaluate the effectiveness of NNTBFV on the ACAS Xu model project, choosing Verification-based and Random-based neural network simplification algorithms as the baselines for NNTBFV. Experiment results show that NNTBFV can effectively approximate the baseline in terms of simplification capability, and it surpasses the efficiency of the random-based method.

Human–Machine Pair Programming (HMPP) is a promising technique in the software development process, which means that software construction can be done in the manner that humans are responsible for developing the program while computer is responsible for monitoring the program in real-time and reporting errors. The Java runtime exceptions in the current version of the software under construction can only be effectively detected by means of its execution. Traditional software testing techniques are suitable for testing completed programs but face a challenge in building a suitable testing environment for testing the partial programs produced during HMPP. In this paper, we put forward a novel technique, called Program Segment Testing (PST) for automatically identifying errors caused by runtime exceptions to support HMPP. We first introduce the relevant involved in this technique to detect index out of bounds exceptions, a representative of runtime exceptions. Then we discuss the methodology of this technique in detail and illustrate its workflow with a simple case study. Finally, we carry out an experiment to evaluate this technique and compare it with three existing fault detection techniques using several programs to demonstrate its effectiveness.

Pointer analysis is the underlying technique of many static analysis tools for vulnerability discovery. It has proved to be effective in identifying a variety of vulnerabilities, such as buffer overflow vulnerabilities and injection vulnerabilities. However, most existing pointer analysis approaches require whole-program availability, i.e. the program to be analyzed should be complete, which may hinder a timely analysis during the coding phase. In this paper, we present two approaches, exhaustive and demand-driven pointer analyses, both of which are applied to a paradigm known as Human–Machine Pair Programming. The ideas enable us to discover security flaws as early as in the coding phase. In this paper, we describe in detail how our approaches maintain flow sensitivity and propagate points-to and taint information in an incremental fashion. We conduct an evaluation of our approaches on SecuriBench Micro and show that the approaches can capture all the potential vulnerabilities in the test cases, though several false alarms are reported.

Abstract Software inspection is a widely-used approach to software quality assurance. Human-Machine Pair Inspection (HMPI) is a novel software inspection technology proposed in our previous work, which is characterized by machine guiding programmers to inspect their own code during programming. While our previous studies have shown the effectiveness of HMPI in telling risky code fragments to the programmer, little attention has been paid to the issue of how the programmer can be effectively guided to carry out inspections. To address this important problem, in this paper we propose to combine Risk Number with Code Inspection Diagram (CID) to provide accurate guidance for the programmer to efficiently carry out inspections of his/her own programs. By following the Code Inspection Diagram, the programmer will inspect every checking item shown in the CID to efficiently determine whether it actually contain bugs. We describe a case study to evaluate the performance of this method by comparing its inspection time and number of detected errors with our previous work. The result shows that the method is likely to guide the programmer to inspect the faulty code earlier and be more efficient in detecting defects than the previous HMPI established based on Cognitive Complexity.

With the growing popularity of Android devices, Android malware is seriously threatening the safety of users. Although such threats can be detected by deep learning as a service (DLaaS), deep neural networks as the weakest part of DLaaS are often deceived by the adversarial samples elaborated by attackers. In this paper, we propose a new semi-black-box attack framework called one-feature-each-iteration (OFEI) to craft Android adversarial samples. This framework modifies as few features as possible and requires less classifier information to fool the classifier. We conduct a controlled experiment to evaluate our OFEI framework by comparing it with the benchmark methods JSMF, GenAttack and pointwise attack. The experimental results show that our OFEI has a higher misclassification rate of 98.25%. Furthermore, OFEI can extend the traditional white-box attack methods in the image field, such as fast gradient sign method (FGSM) and DeepFool, to craft adversarial samples for Android. Finally, to enhance the security of DLaaS, we use two uncertainties of the Bayesian neural network to construct the combined uncertainty, which is used to detect adversarial samples and achieves a high detection rate of 99.28%.

Recommendation systems powered by artificial intelligence (AI) are widely used to improve user experience. However, AI inevitably raises privacy leakage and other security issues due to the utilization of extensive user data. Addressing these challenges can protect users’ personal information, benefit service providers, and foster service ecosystems. Presently, numerous techniques based on differential privacy have been proposed to solve this problem. However, existing solutions encounter issues such as inadequate data utilization and a tenuous trade-off between privacy protection and recommendation effectiveness. To enhance recommendation accuracy and protect users’ private data, we propose ID-SR, a novel privacy-preserving social recommendation scheme for trustworthy AI based on the infinite divisibility of Laplace distribution. We first introduce a novel recommendation method adopted in ID-SR, which is established based on matrix factorization with a newly designed social regularization term for improving recommendation effectiveness. We then propose a differential privacy-preserving scheme tailored to the above method that leverages the Laplace distribution’s characteristics to safeguard user data. Theoretical analysis and experimentation evaluation on two publicly available datasets demonstrate that our scheme achieves a superior balance between privacy protection and recommendation effectiveness, ultimately delivering an enhanced user experience.

Human-Machine Pair Inspection (HMPI) is a novel code inspection technology proposed in our previous work, which is the style that machine will intelligently guide the programmer to carry out inspections of the program code during programming. For large-scale software projects, the efficiency of HMPI needs to be improved due to the inaccurate measurement of the code structure and the excessive inspection scope. In this paper, to alleviate the above deficiencies, we propose the Risk Number, a code evaluation metric generated based on historical error data. The Risk Number is calculated by a statistical tool called regression analysis, which more accurately indicates the relationship between the nested structure of the code and the likelihood of containing bugs than Cognitive Complexity. Additionally, HMPI is supported by utilizing Risk Number to point out high-risk code and program slicing techniques to extract statements that have dependencies on the code to generate checklists, thereby reducing the scope of inspection. We describe a case study to evaluate the performance of this method by comparing its inspection time and number of detected errors with our previous work. The result shows that the method is likely to guide the programmer to inspect the faulty code earlier and be more efficient in detecting defects than HMPI based on Cognitive Complexity.

Pointer analysis is the underlying technique of many static analysis tools for vulnerability discovery. Most existing pointer analysis approaches require whole-program availability, i.e., a program to be analyzed should be complete, which may hinder a timely analysis during the coding phase. By contrast, the attempt of this work is to perform analyses in Human-Machine Pair Programming, where the programs being analyzed are still under construction. Analyzing such incomplete programs enables programmers to discover security flaws as early as in the coding phase. In the paper we describe in detail how our approach maintains flow sensitivity and propagates points-to and taint information in an incremental fashion. We demonstrate the feasibility of our approach by conducting an experiment on a security benchmark. The experiment results show that our approach can capture all the potential vulnerabilities in the test cases in real time, though a number of false alarms are reported.

Abstract Software faults are costly to find and remove from programs. It is better to avoid inserting the faults in the first place. The authors identify requirements‐related faults that can arise during the transformation of formal specifications into programs, analyse each to discover its causes, and propose corresponding fault prevention methods. The approach works by analysing a specification, decomposing it into specification fragments with different levels like components, determining the correct implementation order among the components, and enabling automated code generation for the components and other low‐level specification fragments. The approach seeks to reduce the faults in programs significantly by guiding programmers to work effectively and productively. The authors evaluate the approach's performance experimentally and compare it to the performance of a fault‐prevention method with industry applications.

A deep learning system (DLS) developed based on one software project for defect prediction may well be applied to the related code on the same project but is usually difficult to be applied to new or unknown software projects. To address this problem, we propose a Transferable Graph Convolutional Neural Network (TGCNN) that can learn defects from the lightweight semantic graphs of code and transfer the learned knowledge from the source project to the target project. We discuss how the semantic graph is constructed from code; how the TGCNN can learn from the graph; and how the learned knowledge can be transferred to a new or unknown project. We also conduct a controlled experiment to evaluate our method. The result shows that despite some limitations, our method performs considerably better than existing methods.

With the increasing penetration of the Internet of things (IoT) into people's lives, the limitations of traditional medical systems are emerging. First, the typical way of handling sensitive information can easily lead to privacy disclosure. Second, the medical system is relatively isolated. It is difficult for one medical system to share data with another, and the scope of users' activities is limited within the system boundary. To solve these two problems, we propose a new privacy-preserving medical data-sharing scheme by introducing the authorization mechanism and attribute-based encryption (ABE) based on blockchain, which breaks system boundaries and realizes data sharing among several medical institutions. ABE is used to realize scalable access control. In addition, doctors can share their knowledge to diagnose users by introducing many-to-many matching, which means that patients' health data can be represented by multiple keywords and doctors' expertise can be represented by multiple interests. We provide the correctness and security analysis of our scheme and implement a prototype tool on Ethereum. The experimental results show that our scheme solves the contradiction between the privacy preservation of medical data and the necessity of data sharing.

Machine learning has made significant progress in image recognition, natural language processing, and autonomous driving. However, the generation of adversarial examples has proved that the machine learning system is unreliable. By adding imperceptible perturbations to clean images can fool the well-trained machine learning systems. To solve this problem, we propose an adaptive image denoising framework Adaptive Scalar Quantization (ASQ-FastBM3D). TheASQ-FastBM3Dframework combines theASQmethod with theFastBM3Dalgorithm. The adaptive scalar quantization is the improvement of scalar quantization, which is used to eliminate most of the perturbations.FastBM3Dis proposed to improve the quality of the quantified image. The running time ofFastBM3Dis 50% less than that ofBM3D. Compared with some traditional filter methods and some state-of-the-art neural network methods for recovering the adversarial examples, the accuracy rate of ourASQ-FastBM3Dmethod is 99.73% and the F1 score is 98.01%, which is the highest.

Testing a program based on its specification is necessary to ensure that the program meets its desired functionality. Formal methods, based on some mathematical theories, are often used to enhance the quality of systems but suffer from difficulties in application. The Testing-Based Formal Verification (TBFV) is proposed as an alternative to ensure the correctness of all traversed program paths, but is limited and impractical due to the lack of the capability of dealing with operations (e.g., methods defined in classes) provided in software packages. In this paper, we provide an axiomatic approach to dealing with this problem so as to enhance the capability of the TBFV. In particular, we focus on the Vector, ArrayList, and LinkedList classes in Java. We present both an example to demonstrate how our approach works properly and two small experiments conducted to evaluate the performance of our approach by comparing it with the specification-based testing (SBT). The result shows that our approach is more than 30% superior to the SBT in bug detection.

Software configuration requires that the user sets appropriate values to specified variables, known as configuration parameters, which potentially affect the behaviors of software system. It is an essential means for software reliability, but how to ensure correct configurations remains a great challenge, especially when a large number of parameter settings are involved. Existing studies on misconfiguration diagnosis treat all configurations independently, ignoring the constraints and correlations among different configurations. In this article, we reveal the phenomenon of multi-misconfigurations and present a tool, MMD, for multi-misconfigurations diagnosis. Specifically, MMD consists of two modules: Correlated Configurations Analysis and Primary Misconfigurations Diagnosis. The former determines the correlation among each pair of configurations by analyzing the control and data flows related to each configuration. The latter is responsible for collecting a list of configurations ranked according to their suspiciousness. Combining the outputs of two modules, MMD is able to assist the user in multi-misconfigurations diagnosis. We evaluate MMD on seven popular Java projects: Randoop, Soot, Synoptic, Hdfs, Hbase, Yarn, and Zookeeper. MMD identifies 510 configuration correlations with a 4.9% false positive rate. Furthermore, it effectively diagnoses 22 multi-misconfigurations collected from StackOverflow, outperforming two state-of-the-art baselines.

How can we make software services evolve safely and be long-lived? By designing on the premise of microservices, the services become loosely coupled, which can localise the changes in the system and accelerate the changes. However, from a medium- to long-term perspective, it is not easy to respond to changes in technology trends, business changes including legal revisions, and changes in user requirements among the changing project members. We propose DevFemOps as a way to enhance maintainability and achieve continuous quality improvement, coining the term DevFemOps to place Formal Engineering Methods at the center of the DevOps cycle. We also define the DevFemOps QA engineer as a new role within the agile development squad that is responsible for the quality of the product. In this paper, we will describe how the DevOps cycle, with QA engineers at the center, can bring us closer to the goal of DevFemOps.

Formal specifications can provide a solid foundation for software development and support for techniques of software quality assurance, such as specification-based inspection and testing. To ensure that these techniques can be applied effectively in practice, efficiently and accurately understanding specifications becomes extremely important. While this may be relatively easy for well-trained developers in formal methods, it can be rather difficult for computer since computer does not easily understand specifications. This difficulty poses a challenge for realizing automatic specification-based verification techniques that are in high demand for reducing development cost and improving software reliability. In this paper, we address this problem by discussing how the formal specification can be transformed into a knowledge graph to provide comprehensible, well-organized details of the specification for developers and computers. The transformation is done by extracting and storing information about attributes of each component and by establishing relationships between components in a formal specification. We elaborate on a top-down approach of constructing a knowledge graph from a specification, including creating an ontology, designing the Entity–Relationship (ER) diagram of the relational database based on the created ontology, extracting and storing attribute and relationship information in the relational database, mapping ontology to its instances and relational data to RDF triples, and displaying knowledge graph. Further, we present a case study to show how our approach works on the formal specification of an ATM system. Finally, we describe three experiments to evaluate its performance in improving specification readability, effectively guiding inspectors to establish traceability links between specifications and programs, and detecting defects through program inspection, respectively.

While promoting the intelligence in industrial production, Industry 4.0 has also caused privacy leaks concurrently. As a possible solution, the existing personalized federated learning relies too much on a good global model to fine-tune or limit local drift, which lacks intelligent cognitive ability. When faced with heterogeneous data or poisoning attacks, even a few low-quality local models will affect the whole federation effect. In this article, we design a cognitive personalized federated learning (CPFL) mechanism for Industry 4.0, which can selectively improve the collaboration capabilities between more relevant devices. We use the parameters in the local training process as the cognitive basis and calculate Earth mover’s distance to quantify the differences between different models. When the gradient distribution is closer, the local data are more similar. By adaptively adjusting the weight distribution during the aggregation process, self-learning and cooperative learning are balanced, and the interference of heterogeneous data on the federated training process is reduced. Therefore, the global model can better fit most heterogeneous industrial data and achieve personalization. Comparative experimental results show that our proposed CPFL mechanism can increase the average accuracy of personalized models by 5%–10% in non independent and identically distributed situations, and it has certain effects against poisoning attacks and noise interference.

Software defect prediction is aimed at helping developers to quickly locate defective components in the code repository and thus better allocate resources. However, most of the current traditional defect prediction methods mainly depend on the design of static metrics, but these methods ignore the semantic and structural information of the code. As a result, researchers have turned to building models by extracting semantic features from code through abstract syntax trees. In this article, we introducegated homogeneous fusion networkfor defect prediction namely GHFNet, jointing high-level semantic feature extraction and weighted static feature extraction. Through the mechanism of homogeneous gating fusion, weights are adaptively assigned to the two types of features based on the correlation of these features to form fused features for defect prediction in the code. Experimental results show that the proposed approach is a significant improvement. Specifically, for the reference method we present GHFNet improved from 9.4 to 15.2 percentage points in effort-unaware scenarios (F-measure) and from 3.7 to 8 percentage points in effort-aware scenarios (Popt) for defect prediction.

Testing a program to confirm whether it consistently implements its requirements specification is a necessary but time-consuming activity in software development. Automatic testing based on specifications can significantly alleviate the workload and cost, but faces a challenge of how to ensure that both the user’s concerns in the specification and possible execution paths in the program are all covered. In this paper, we describe a new method, called “Vibration-Method” or simply “V-Method”, for automatic generation of test cases and test oracle from model-based formal specifications, aiming to address this challenge. The proposed method is suitable for testing information systems in which rich data types are used. Supporting the principle of “divide and conquer”, the method provides a specific technique for generating test cases based on functional scenarios defined in the specification, test case generation criteria, automatic test case generation algorithms, and a well-defined mechanism for deriving test oracle. We elaborate on the method by discussing how initial test cases can be automatically generated, how additional necessary test cases are produced using the “vibration” technique, and how a test oracle can be automatically derived for a group of test cases. We also describe a controlled experiment to evaluate the effectiveness of the method and discuss the important issues in relation to the performance and applicability of the method.

Software defect prediction plays a significant role in the software development cycle but suffers from many difficulties. In this paper we propose a novel deep learning model (including algorithms) called Extractor, Parser, and Reviewer (EPR) for defect prediction in software. Two different networks, recurrent neural networks (RNNs) and one-dimensional convolutional networks(ODCNs), are employed by the EPR for different purposes. RNN is utilized to extract contextual features to represent semantic dependencies between code tokens and ODCN acts as a parser to establish dependencies between semantic features. Meanwhile, the attention mechanism of the two networks is used as a reviewer to assign different weights from location information to the importance of the features, respectively. Our proposed model is validated by the PROMISE repository, and the results show that the proposed model in this paper significantly outperforms several existing algorithms.

Linking the components in a formal specification to those in the corresponding program is a prerequisite for formal specification-based program fault detection. Existing traceability link techniques for reducing manpower and time cost suffer from the limitation in effectiveness due to over dependency of textual similarity. Unlike the existing work, this paper presents an automatic method for constructing traceability links between SOFL formal specifications and Java codes, taking semantical, structural, functional, and relational similarities measures into account. It operates at multiple levels of a formal specification, such as data flows, processes, and modules, to establish finegrained link relationships between artifacts. Further, a comparative evaluation of the proposed method, using two selected modules of the SOFL formal specification of a critical ATM system and its Java implementation with 951 code of lines, demonstrates an improvement in precision and more generality than existing latent semantic indexing that is an information retrieval-based method.

The test case generation technique from formal specifications called the Vibration Testing Method has been put forward. This technique is aimed at gaining coverage of program paths and detecting bugs, even though the test cases are generated only based on specifications. Since it lacks a supporting tool currently, its application is inefficient and errorprone. In this paper, we tackle this problem by describing a supporting tool for the method that we have developed over the last two years. The tool does not only automatically generate test cases based on the Vibration Method, but also can automatically analyze test results. Further, it can also automatically “prove” theorems to support practical formal verification of program properties. During the development of the tool, we have made some important improvements to the techniques of the method for automatic test case generation. We have conducted a small experiment to evaluate our tool and the improved Vibration Method. The experiment result shows that a 12% improvement on the previous method is made.

Automatic test oracle generation is a bottleneck in realizing full automation of the entire software testing process. This study proposes a new method for automatically generating a test oracle for a new test input on the basis of several historical test cases by using a backpropagation neural network (BPNN) model. The new method is different from existing test oracle techniques. Specifically, our method has two steps. First, the values of variables are collected as training data when several historical test inputs are used to execute the program at different breakpoints. The test oracles (pass or fail) of these test cases are utilized to classify and label the training data. Second, a new test input is used to execute the program at different breakpoints, where the trained BPNN prediction model automatically generates its test oracle on the basis of the collected values of the variables involved. We conduct an experiment to validate our method. In the experiment, 113 faulty versions of seven types of programs are used as experimental objects. Results show that the average prediction accuracy rate of 74,651 test oracles is 95.8%. Although the failed test cases in the training data account for less than 5%, the overall average recall rate (prediction accuracy of test case execution failure) of all programs is 78.9%. Furthermore, the trained BPNN can reveal not only the impact of the values of variables but also the impact of the logical correspondence between variables in test oracle generation.

As recommendation systems continue to evolve, researchers are using trust data to improve the accuracy of recommendation prediction and help users find relevant information. However, large recommendation systems with trust data suffer from the sparse trust problem, which leads to grade inflation and severely affects the reliability of trust propagation. This paper presents a novel research on sparse trust data mining, which includes the new concept of sparse trust, a sparse trust model, and a trust mining framework. It lays a foundation for the trust-related research in large recommended systems. The new trust mining framework is based on customized normalization functions and a novel transitive gossip trust model, which discovers potential trust information between entities in a large-scale user network and applies it to a recommendation system. We conducts a comprehensive performance evaluation on both real-world and synthetic datasets. The results confirm that our framework mines new trust and effectively ameliorates sparse trust problem.

Symbolic execution is a powerful technique for automating software testing to detect many types of errors such as memory errors and assertion violations. However, it encounters the problem of path explosion, and by using only assertions, it still lacks the capability of going deep into checking the functional correctness of a path based on corresponding formal specifications. To address these problems, we propose a specification-based incremental testing method with symbolic execution, called SIT-SE, providing a much more rigorous way to automatically check the functional correctness of all the discovered program paths, by introducing theorems (instead of assertions) for path correctness and branch sequence coverage algorithm for guiding a moderate path exploration. Compared with Hoare logic for proving the correctness of an entire program, a theorem in the SIT-SE is made for verifying the correctness of a program path. The proposed method carefully treats the relationship between a path condition and the specification in a theorem to restrict the monotonous path exploration, whereas traditional concolic testing methods roughly use one test data to determine the path correctness by assertions during long path searching. We use a classic case to demonstrate how the method works and conduct an experiment to evaluate the performance of both the proposed method and the commonly used well-known concolic testing tool KLEE. The experimental results show that our method SIT-SE is effective and outperforms KLEE in detecting faulty paths based on specifications.

The rapid development of safety-critical systems eagerly demands for the formal verification or enormous testing to ensure the correctness of programs. Testing-based formal verification with symbolic execution (TBFV-SE), a technique that integrates both formal verification and testing, taking the advantages of both methods without so much cost to meet such need. In order to further pinpoint the problematic positions in the code when TBFV-SE gives the incorrect program paths, we describe a fault localization algorithm to do this work through making use of the information provided by TBFV-SE. A case study demonstrates that our algorithm can more effectively and efficiently shrink the scale of suspicious lines of the code.

As the current specification-based testing (SBT) face some challenges in test case generation for regression testing, we propose a new method for efficient test case generation that combines formal specifications with genetic algorithm (GA). This method mainly reforms formal specifications though GA to generate inputs that can kill as many as possible mutants of the target program under test. For case study, two classic examples are presented to demonstrate the efficiency of this method. The result shows that this method is able to help efficiently generate useful test cases to uncover all the program mutants, which contributes to further maintenance of software.

Testing-Based Formal Verification (TBFV) is a rigorous and potentially automated approach to verifying the correctness of traversed program paths based on specification-based testing and Hoare logic, but its capability is limited due to the fact that Hoare logic may not be applicable. To address this challenge, we propose to use symbolic execution to replace Hoare logic in the existing TBFV, thus enhance the capability of TBFV. We call the newly proposed approach TBFV-SE (TBFV - Symbolic Execution). The advantage of TBFV-SE over the existing TBFV lies in its applicability to wide range of programs while preserving its characteristic of full automation. We descirbe the principle of TBFV-SE and present two case studies to demonstrate its feability and usability. We also discuss the condition under which TBFV-SE can be effectively used and potential challenges in building a tool support.

In the recent times, software security has gained a great deal of attention in the Software Development Life Cycle due to increased cases of reported cyber threats and incidents. A considerable number of cyber-attacks targeting financial systems has made security be the most critical feature in banking systems. However, establishing security requirements for these applications can be a challenging task because the activities and measures demanded by their requirements calls for a clear understanding and implementation without any degree of ambiguity. In order to address this, we propose a new framework; Security Requirement Engineering with Structured Object Oriented Formal Language (SRESOFL), while giving special focus on financial applications. The framework seeks to offer a weaving approach where security requirements and the functional system requirements are fused together during the system`s requirement specification phase. We will illustrate the applicability of the SRESOFL framework with a case study on the development of a mobile banking application.

Testing a program based on its specification is necessary to ensure that the program meets its desired functionality. In this paper, we describe a specification-based testing method that can reduce the cost and ensure the correctness of the tested program paths. The cost of testing is reduced by guaranteeing that the same path can be repeatedly tested automatically without the need to executing the path repeatedly. The correctness of the path is guaranteed by means of automatically applying the relevant parts of the Hoare logic. We also present the design and implementation of a prototype tool that supports the testing method.

Software design has been well recognized as an important means to achieve high reliability, and formal specification can help enhance the quality of design. However, communications between the designer and the user can become difficult via formal specifications due to the potentially complex mathematical expressions in the specification. This difficulty may lead to the situation where the user may not be closely involved in the process of constructing the specification for quality assurance. To allow formal specification to play more effective roles in software design, we put forward a new approach to deal with this problem in this paper. The approach is characterized by integrating specification animation-based inspection into the process of constructing formal design specifications. We discuss the underlying principle of the approach by explaining how specification animation is utilized as a reading technique for inspection to validate, and then evolve, the current specification towards a satisfactory one. We describe a prototype software tool for the method, and present a case study to show how the method supported by the tool works in practice.

Functional scenario-based specification animation is a practical and effective technique for validating formal specifications but faces a scenario explosion problem. In this paper, we tackle this problem by proposing a new approach to selecting only consistent and meaningful functional scenarios in order to reduce the number of scenarios for animation. We define the concept of consistency for functional scenarios and describe how each of them can be automatically checked by means of a testing-based formal verification technique. We have applied the proposed technqiue to a railway card system to validate its applicability and present an example extracted from the application to illustrate how the proposed technqiues works in practice.

Informal and semi-formal specifications are commonly adopted for requirements engineering (RE), especially for customer-oriented system development projects, but their validity with respect to the user's requirements is usually difficult to perform. The common reason for the difficulty is that the specifications are often misinterpreted by the stakeholders due to the ambiguity of the natural language or graphical notation used in writing the specifications. This paper describes a tool to assist the animation of informal and semi-formal specifications intuitively and comprehensively for their validation. The underlying animation principle is called SOFL Requirements Specification Animation Framework (SOFL-RSAF). The framework integrates specification animation into the SOFL method for constructing specifications and is supported by a prototype add-in tool.

Despite the effectiveness of requirements formalization in producing accurate requirements documentation, thistechnique can hardly be accepted by software industry mainlydue to the difficulty in manipulating formal notations by practitioners. To handle the challenge, this paper describes aninteractive tool for supporting requirements formalization basedon specification pattern knowledge comprising a set of inter-relatedspecification patterns. Each pattern defines the knowledge forformalizing one kind of function, including derivation knowledgefor guiding the clarification of the function and transformation knowledge for formally representing the clarified function. The tool derives necessary function details of the intendedrequirement through interactions by applying the derivationknowledge and transforms these details into formal specificationsby applying the transformation knowledge.

Formal specification has proved to be an effective technique for precisely defining software functionality, but validating it against the user's requirements still remains a challenge. In this paper, we propose a novel and practical review approach that utilizes specification animation and trace links to support the reviewing of formal specifications for their validation. The scenario-based animation method dynamically presents the specification to the reviewer by means of "executing" it in a step-by-step manner. It is adopted as a reading technique to guide the reviewer to read the specification and provides him with clear review targets. The trace links that connect the specification to the user's original requirements supply the reviewer with necessary information for determining whether defects are found. We first explain the scenario-based animation and trace links respectively and then propose a group of criteria for validating the formal specification. A case study is described to illustrate the review process at the end of the paper.

Formalizing requirements in formal specifications usually requires high skills for abstraction and experience in using the formal notation in which the specification is written. This poses a challenge to many practitioners who have to deal with realistic systems within the required schedule and budget. To handle this challenge, a pattern system has been proposed for computer-aided construction of formal expressions. It organizes various inter-related patterns on computer, each of which deals with the formalization of a kind of informal ideas. But how to represent such knowledge to facilitate its automatic utilization and maintenance remains a problem. This paper presents an approach to representing and utilizing the pattern knowledge on the basis of a formal definition of the pattern system. The application process of the pattern system is described in HFSM (Hierarchical Finite State Machine) and treated as knowledge. By performing a proposed algorithm, necessary information can be retrieved from the HFSM for capturing informal requirements and automatically generating formal expressions. We also describe a prototype tool that implements the approach and present a case study on modeling a bank data management system.

Automatic transformation from informal requirements to formal specifications is an important but challenging topic in software engineering. The major challenge stems from the fact that informal requirements are usually too abstract to provide sufficient information required for completing the formal specification. In this paper, we propose an approach to guiding the clarification of requirements to prepare for their automatic formalization on the basis of specification patterns. Each pattern provides a template for clarifying one kind of requirement by showing how it is decomposed into a set of requirement elements. Each element is formally defined to denote one of the attributes of the requirement. Clarifying a requirement is actually a process of assigning values to the relevant elements according to their formal definitions. An example of Automated Teller Machine (ATM) system is presented to illustrate the approach.

Service-based software modeling is considered as an effective technique for developing high-quality service-based systems. One major challenge of this approach is how to effectively utilize existing software services in the process of system modeling to ensure the reliability of the system while reducing the development cost and effort. In this paper, we propose a novel formal engineering framework by integrating an evolutionary service selection approach into a formal engineering method to tackle this problem. In the framework, initial requirements are gradually transformed into a formal design specification through three steps during which existing services are discovered, filtered, selected, and employed. Candidate services are discovered through a keyword-based searching. A static behavior analysis technique is then used to filter the candidate services and a specification-based testing method is adopted to rigorously select the candidate services. The selected services are finally incorporated into the formal design model of the system. We present an empirical case study that was conducted for evaluating the usability of our framework by applying it to develop a travel agency system. The result of the study demonstrates several advantages of the framework over existing approaches but meanwhile also shows some limitation in practice.

The validation of formal specifications before their implementation can help to detect errors of systems in early stages of development and reduce the entire cost significantly. Formal specification animation is developed as an effective technique for this purpose. Animation gives the end users and field experts an intuitive way to observe the operational behavior of specification without being distracted by its complex syntax. Several tools have already been built to support specification animation. But most of these tools need a translation from a formal specification language to an executable programming language. In this paper, we propose a novel animation approach called Automatic Functional Scenarios-based Animation. This approach uses data as connection among independent operations involved in a specific behavior to "execute" specifications, and does not translate them to program. We explain how to generate necessary data for animation by modifying an automatic operation function scenario-based test case generation method, and present a case study of applying this animation approach to SOFL specification.

Low-fidelity prototyping has been increasingly adopted in software development to facilitate the communication between the developer and the end-user, since it can be simply realised without the need for programming. However, this technique is not mature enough as it lacks a systematic approach to build prototypes and capture user feedback. In this paper, we present a method that provides a systematic way to build low-fidelity prototypes from informal specifications and to collect user feedback for completing or refining the requirements. Three steps are essential for this method. The first step is to derive implementation architecture of the prototype from the specification by determining the design properties of the required functions and to define their relationships. The second step is to construct the prototype based on the architecture using the animation tool in Microsoft PowerPoint. The third step is to gather user's feedback using specific forms during low-fidelity prototyping. We have applied this method to the development of a web-based Travel Agent System. The result shows that our approach is effective in ensuring the quality and efficiency of communication and software requirements, although it still has room for further improvement.

Software inspection is a static analysis technique that is widely used for defect detection, but which suffers from a lack of rigor. In this paper, we address this problem by taking advantage of formal specification and analysis to support a systematic and rigorous inspection method. The aim of the method is to use inspection to determine whether every functional scenario defined in the specification is implemented correctly by a set of program paths and whether every program path of the program contributes to the implementation of some functional scenario in the specification. The method is comprised of five steps: deriving functional scenarios from the specification, deriving paths from the program, linking scenarios to paths, analyzing paths against the corresponding scenarios, and producing an inspection report, and allows for a systematic and automatic generation of a checklist for inspection. We present an example to show how the method can be used, and describe an experiment to evaluate its performance by comparing it to perspective-based reading (PBR). The result shows that our method may be more effective in detecting function-related defects than PBR but slightly less effective in detecting implementation-related defects. We also describe a prototype tool to demonstrate the supportability of the method, and draw some conclusions about our work.

Currently most web services are published without sufficient functional behavior descriptions, which makes it difficult for developers to accurately select services according to the expected functions of their target systems. In this paper, we propose a formal specification-based testing approach to accurate service selection. Requirements upon candidate services are refined into formal specifications in terms of functional scenarios. Test cases for each service operation are basically generated from its associated functional scenarios. Since the internal variables of stateful services are not allowed to be directly monitored from user-end, state transitions of these internal variables can only be checked through running inter-related operations in combination. In particular, functional scenario pairs are used as the foundation for test sequences generation so that potential combinations of interrelated operations can be tested. Conformance of candidate services with respect to users' requirements is determined based on the analysis of testing results. A running example is illustrated to demonstrate the application of this approach. We have also conducted experiments to evaluate the feasibility and the effectiveness of our conformance testing approach.

Several approaches to test case generation based on formal specifications have been put forward, but how to automatically generate test cases to ensure that all of the representative program paths of the corresponding program are traversed still remains an open problem. In this paper, we describe a new technique called "Vibration" method to tackle this problem. The method focuses on a heuristic process of generating test cases, collecting traversed paths, and removing the bugs detected, based on a single test condition of a functional scenario until all the corresponding program paths are traversed or a stopping testing condition is met. The test case generation is fully automatic, in the sense that all the criteria can be implemented by algorithms in a software tool. We describe the criteria and algorithms for test case generation and for stopping a testing process.

Automatic specification-based testing has long been a goal of software engineering, but due to various challenges and difficulties, the goal still remains far from realized. If the specification is informal, full automation would be impossible in general. Formal specification improves the situation, but there are many barriers lying ahead. Automatic test set generation can be difficult to meet high standard, but test result analysis for determining the existence of bugs and debugging for locating the bugs and deciding their nature seem to be even more challenging. This paper systematically discusses all of the major challenges in automatic specification-based testing, and describes some possibilities to deal with the challenges. Some open but interesting problems are presented to inspire future research in the field.

Software risk comes mainly from its poor reliability, but how to effectively achieve high reliability still remains a challenge. This paper puts forward a framework for systematically integrating formal specification, review, and testing, and shows how it can be applied to effectively eliminate errors in the major phases of software development process to enhance software reliability. In this framework, requirements errors can be removed and missing requirements can be identified by formalizing requirements into formal specifications whose validity can be ensured by rigorous review. The valid specification can then be used as a firm foundation for implementation and for rigorous inspection, testing, and walkthrough of the implemented program. We discuss how formalization, review, and testing work together at different levels of software development to improve software reliability through detecting and removing errors in documentation.

Functional scenario-based test case generation is an important technique for specification-based testing and it can be fully automated. The vital first step of achieving the automation is automatic transformation from a formal specification into an equivalent functional scenario form from which all functional scenarios are derived. In this paper, we first explain the concepts of the functional scenario form and the functional scenario in the context of a VDM operation specification, and then discuss the techniques for the transformation implemented in a software tool we have built. The techniques for discussion include (1) transformation from compound expressions into predicate expressions, (2) transformation from quantified expressions into non-quantified expressions, (3) replacing implications and equivalences in predicate expressions, (4) transformation from predicate expressions into functional scenario forms, and (5) the derivation of the testing condition from a functional scenario for test case generation. Based on these transformations, the tool can also automatically produce test cases to meet required conditions.

Writing formal specifications can help developers understand users' requirements, and build a solid foundation for implementation. But like other activities in software development, it is error-prone, especially for large-scale systems. In practice, effective detection of specification errors still remains a challenge. In this paper, we put forward a rigorous, systematic method for the inspection of model-based formal specifications. The method makes good use of the well-defined consistency properties of a specification to provide precise rules and guidelines for inspection. The inspection process utilizes both well-defined expressions derived from the specification and human inspectors' judgments to find errors. We present a case study of the method by describing how it is applied to inspect an Automated Teller Machine (ATM) software specification to investigate the method's feasibility, and explore potential challenges in using it. We also describe a prototype software tool including its functions and distinct features to demonstrate the tool supportability of the method.

Service-oriented computing advocates the development of new software or services on the basis of existing services. This paradigm shows a great potential of achieving high productivity and low cost, but it faces a challenge in efficiently and correctly using existing services in producing a new application and ensuring its reliability. Building a formal model using a formal specification language allows the developer to thoroughly understand what existing services are needed for the new application, but how to construct the model so that it can effectively facilitate the developer to recognize the appropriate services still remains an open problem. In this paper, we describe an approach to applying the SOFL formal engineering method to the modeling of a service-oriented system by means of a case study. In particular, we focus on the issue of how to apply the SOFL three-step modeling approach to the construction of a formal specification for a service-based system, exploring the general principle and specific techniques for reusing existing services in developing a system model.

The application of specification-based program verification techniques (e.g., black-box testing, formal proof) faces strong challenges in practice when the gap between the structure of a specification and that of its program is large. This paper describes a view-based program review approach to addressing these challenges. The essential idea of the approach is first to derive comparable views from the specification and program, and then detect and eliminate the violations of structural consistency in the program views on the basis of a set of criteria. We also developed a prototype tool to support the review approach, and conducted a case study to assess the effectiveness of the approach.

Insulin pump system is a safety-critical embedded system controlling the amount of injection of insulin to diabetics based upon their blood glucose levels, and the high reliability of the software used in the pump is crucial. One way to achieve the high reliability of software is to build an accurate and complete model through effective analysis and specification, and to implement the system based upon the specification. In this paper, we describe how the SOFL formal engineering method is applied to develop a specific insulin pump system in practice. In particular, we focus on the issue of how the three-step modeling approach advocated by the SOFL method, which includes informal, semi-formal, and formal specifications, is utilized to obtain a precise and valid specification of the embedded software for the insulin pump system. We also discuss how the specification benefits the implementation of the system, and report our experience and lessons learned.

Effective tool support is crucial for successfully applying software review techniques in practice. In this paper, we describe the design and implementation of a software tool to support an approach to reviewing programs on the basis of their formal specifications. The approach was initially proposed in our previous publication to improve the rigor, repeatability, and effectiveness of existing code review methods. We also present a case study in which we reviewed an ATM system to assess the performance of the review approach when used with the software tool. The results of the case study show that the approach is effective in detecting errors in programs and the tool is helpful in enhancing the efficiency of the review process.

Program review is a practical and cost-effective method for detecting errors in program code. This paper describes our recent work aiming to provide support for revealing errors which usually arise from inappropriate implementations of desired specifications. In our approach, the SOFL specification language is employed for specifying software systems. We provide a framework that guides reviewers to compare a code with its specification for effective detection of potential defects.

Program review is an effective means for enhancing software quality. In this paper we describe the design of a software tool to support our proposed "function-path" approach to reviewing programs based on SOFL specifications. The approach includes four steps: (1) deriving all the functional scenarios from a formal specification, (2) generating all the necessary program paths in a program, (3) establishing the mapping between the functional scenarios in the specification and the program paths as implemented functions in the program, and (4) reviewing all the program paths against their functional scenarios in the specification.

Domain testing, a technique for testing software or portions of software dominated by numerical processing, is intended to detect domain errors that usually arise from incorrect implementations of desired domains. This paper describes our recent work aiming to provide support for revealing domain errors using formal specifications. In our approach, formal specifications serve as a means for domain modeling. We describe a strong domain testing strategy that guide testers to select a set of test points so that the potential domain errors can be effectively detected, and apply our approach in two case studies for test cases generation.

Software review is an effective means to enhance the quality of software systems. However, traditional review methods emphasize the importance of the way to organize reviews and rely on the quality of the reviewers' experience and personal skills. In this paper we propose a new approach to rigorously reviewing programs based on their formal specifications. The fundamental idea of the approach is to use a formal specification as a standard to check whether all the required functions and properties in the specification are correctly implemented by its program. To help investigate the effectiveness and the weakness of the approach, we conduct two case studies of reviewing two program systems that implement the same formal specification of "A Research Management Policy" using different strategies, and present the evaluation of the case studies. The results show that the review approach is effective in detecting faults when the reviewer is different from the programmer, but less effective when the reviewer is the same as the programmer.

Condition data flow diagrams (CDFDs) are a formalized notation resulting from the integration of Yourdon Data Flow Diagrams, Petri Nets, and pre-post notation. They are used in the SOFL (Structured Object-Oriented Formal Language) specification language to describe the architecture of formal specifications for network protocols and general dependable systems by defining data flow communications among processes. A large-scale specification is usually modeled as a hierarchy of CDFDs resulting from decomposing processes at various levels into CDFDs. To ensure that a decomposed CDFD is correct with respect to its high level process, verification is essential. However, how to verify rigorously the correctness of CDFDs is still an open problem. We address this problem by establishing a logical system consisting of inference rules for reasoning about CDFDs, and putting forward both formal proof and specification simulation as potential methods for correctness verification. We also give algorithms for deriving pre and postconditions of CDFDs and examples of verifying their correctness.

Review task tree (RTT) is a comprehensible notation for expressing review tasks in rigorous review of formal specifications. It has a mechanism for evaluating the final review result based on the review results of all the members (atomic tasks) of its minimal cutset. However, the notation does not provide any method for actually reviewing the atomic tasks. We present a way to utilize a specification testing method for rigorous review of the atomic tasks. Strategies for generating test cases for each kind of RTT are described and explained with examples. A small case study is conducted using the proposed technique, and the result is analyzed to show the benefit and the potential limitation of the technique.

Abstract Although the majority of software testing in industry is conducted at the system level, most formal research has focused on the unit level. As a result, most system‐level testing techniques are only described informally. This paper presents formal testing criteria for system level testing that are based on formal specifications of the software. Software testing can only be formalized and quantified when a solid basis for test generation can be defined. Formal specifications represent a significant opportunity for testing because they precisely describe what functions the software is supposed to provide in a form that can be automatically manipulated. This paper presents general criteria for generating test inputs from state‐based specifications. The criteria include techniques for generating tests at several levels of abstraction for specifications (transition predicates, transitions, pairs of transitions and sequences of transitions). These techniques provide coverage criteria that are based on the specifications and are made up of several parts, including test prefixes that contain inputs necessary to put the software into the appropriate state for the test values. The test generation process includes several steps for transforming specifications to tests. These criteria have been applied to a case study to compare their ability to detect seeded faults. Copyright © 2003 John Wiley & Sons, Ltd.

SOFL (structured-object-based-formal language) has been extended to a formal object-oriented language and method while keeping its structured features. This extension allows powerful object-oriented reuse mechanisms, such as class inheritance and object composition, to be utilized in the early design phases. This paper presents the semantics for this extended SOFL, and further demonstrates the extendibility and reusability of the object-oriented semantic models of SOFL.

Specification simulation is an approach to verifying and validating specifications by well-selected sample data. In this paper we put forward a technique for simulation of formal specifications in order to detect potential faults and validate their desired functions. The important benefit of this technique is it allows us to simulate implicit specifications, which are usually defined with a pair of pre- and postconditions and may not be executable. We discuss ways of simulation case generation, evaluation of logical expressions, and simulation result analysis, and demonstrate how they are applied in practice by examples.

Complete and accurate functional requirements are the foundation for valid specification refinement and correctness verification of implemented software systems when they are developed with a formal method. However, capturing quality requirements is a difficult task, and there is a lack of well-defined and effective technique that solves the problem as well. We argue that the refinement technique used in conventional formal methods for transforming formal specifications into programs is actually an effective technique for capturing the functional requirements. We define the completeness of formal specifications and explain by examples how it can be achieved.

We present an integrated approach to support both top-down and bottom-up design of software systems by combining UML (Unified Modeling Language) and the Formal Engineering Method SOFL (Structured Object-oriented Formal Language). We demonstrate by examples that the top-down principle used in conventional Structured Design can be effectively utilized to carry out object-oriented design that is usually seen as a way to suit bottom-up analysis and design. Furthermore, we also explain how the integrated approach helps to improve the preciseness and understandability of design documentations.

SOFL is a formal language and method for system specification and design. As a language it is an integration of Petri nets, data flow diagrams, and VDM-SL. As a method it is a combination of a structured method and object-oriented method. We introduce a graphical user interface (GUI) for supporting the construction of SOFL specifications, and a tool for testing SOFL specifications. With those tools it would be easy to construct a SOFL specification that consists of condition data flow diagrams, modules, and classes and to ensure its consistency and validity.

An application domain is defined as a family of systems that have some features in common and others that differentiate them. A domain model is a multiple view object oriented analysis model for the application domain that reflects the common aspects and variations among the members of the family of systems that constitute the domain. The paper describes the integration of the domain modeling method for analyzing and modeling families of software systems with the SOFL formal specification language. Aggregation hierarchies and generalization/specialization hierarchies are depicted using the UML static modeling notation. Object communication diagrams are depicted using the SOFL condition data flow diagram notation. SOFL is used for the formal specification of the kernel, optional and variant classes.

How to effectively apply formal methods under schedule constraints to develop real systems is an important issue to address. We report our recent experience in the application of SOFL (Structured Object-based Formal Language) to developing a University Information System. The intention of the study is to investigate whether and how formal methods can benefit the development of non-safety critical systems with time constraints. We have found that if used appropriately, formal methods can help to save time, to improve the accuracy of discussions and communications, to facilitate transformations from specifications to design, and then to programs. On the other hand, we have also found that formal specifications in the style of pre- and postconditions can be difficult to write; formal specifications without reviews may involve mistakes; and satisfactory formal specifications that serve as the reliable documents for development and maintenance may be completed only throughout the entire development process.

This paper presents general criteria for generating test inputs from state-based specifications. Software testing can only be formalized and quantified when a solid basis for test generation can be defined. Formal specifications of complex systems represent a significant opportunity for testing because they precisely describe what functions the software is supposed to provide in a form that can easily be manipulated. These techniques provide coverage criteria that are based on the specifications, and are made up of several parts, including test prefixes that contain inputs necessary to put the software into the appropriate state for the test values. The test generation process includes several steps for transforming specifications to tests. Empirical results from a comparative case study application of these criteria are presented.

One of the primacy concerns in developing computer embedded safety-critical systems is how to develop quality software. Software must fulfill its functional requirements and must not contribute to the violation of safety properties of the entire system. To this end, capturing error free and satisfactory functional requirements is crucial before proceeding to the subsequent development phases. We describe an approach to specifying and verifying software for safety-critical systems with the practical formal method SOFL (Structured-Object-based-Formal Language). Requirements specification focuses on the functionality of the software, but with the consideration of safety constraints and its interaction with the surrounding operational environment. The verification of specifications can be carried out using three techniques: data flow reachability checking, specification, testing, and rigorous proofs, respectively. We apply this approach to a realistic railway crossing controller for a case study and analyzes its result.

In current OO design, most of the existing (semi-formal) methods use classes or objects as the basic unit of design. However it is increasingly recognised that classes are not the best focus for design. Typical design artefacts are about groups of objects and the way they interact In the Catalysis project, we use the term frameworks for descriptions of groups of objects, their relationships, division of responsibilities, and interactions. The power of frameworks lies in the fact that interactions can also occur at the level of frameworks. In a previous paper we defined a framework formally as a (first-order) many-sorted theory with a model theoretic semantics and showed how it can be represented using a pictorial notation for practical system development. However we considered only frameworks that do not interact with one another In this paper we discuss frameworks that interact with one another and show that such frameworks are very powerful tools for formal OO design.

FRSM (Formal Requirements Specification Method) is a structured formal language and method for requirements analysis and specification construction based on data flow analysis. It uses a formalized DeMarco data flow diagram to describe the overall structure of systems and a VDM-SL like formal notation to describe precisely the functionality of components in the diagrams. This paper first describes the formal syntax and semantics of FRSM and then presents an example of using the axiom and inference rules given in the definition of the formal semantics for checking consistency of specifications. A case study of applying FRSM to a practical example is described to demonstrate the principle of constructing requirements specifications and to uncover the benefits and deficiencies of FRSM.

Formal methods have yet to achieve wide industrial acceptance for several reasons. They are not well integrated into established industrial software processes, their application requires significant abstraction and mathematical skills, and existing tools do not satisfactorily support the entire formal software development process. We have proposed a language called SOFL (Structured-Object-based-formal Language) and a SOFL methodology for system development that attempts to address these problems using an integration of formal methods, structured methods and object oriented methodology. Construction of a system uses structured methods in requirements analysis and specifications, and an object based methodology during design and implementation stages, with formal methods applied throughout the development in a manner that best suits their capabilities. The paper describes the SOFL methodology, which introduces some substantial changes from current formal methods practice. A comprehensive, practical case study of an actual industrial Residential Suites Management System illustrates how SOFL is used.

SOFL (Structured-Object-Based-Formal Language) is a formal language and method for practical systems development. As a language, it integrates data flow diagrams, VDM-SL, and Petri nets to provide a graphical and textual formal notation for specification construction. Previous publications introducing SOFL are based on its informal semantics. We provide a formal operational semantics which gives a firm foundation for consistent understanding and application of SOFL in practical systems development. Development of the semantics, and application of SOFL to practical systems, have led to some changes in the original definitions. This formal semantics will serve as a firm foundation for building an effective support environment for SOFL.

Refinement of operations is well defined in terms of refinement rules and is considered as a reasonable discipline for software development. This paper, however, observes that refinement is not sufficient to serve this role for the entire software development process and then proposes evolution for substitution. We show that refinement is indeed a special case of evolution and evolution is transitive. A small case study is given to demonstrate that using evolution rather than refinement as the discipline for software development is a more practical approach. The idea presented in this paper may be controversial, but the author believes that this idea is more useful, practical, and instructive than refinement approach, and expects to inspire more discussions about this issue.

Summary form only given, as follows. A major challenge for formal methods is to effectively address the needs of industry and achieve wide acceptance. This challenge remains unmet, as formal methods are difficult to use and their application consumes prohibitive amounts of resource. Much research on the integration of available formal methods (e.g. Z, VDM, B-method) and either structured methodology or object-oriented methodology has been conducted to make formal methods more practical, but with limited success. No attempt has yet been made to integrate the three approaches of formal methods, structured methodology and object-oriented methodology to take advantage of the desirable features of the three approaches. As one approach to the solution of these problems, we propose a language called SOFL (Structured Object-oriented Formal Language) for system development. It supports the concept that a system can be constructed using the structured methodology in the early stages of its development, and by using object-oriented methodology at later, more detailed levels. During the complete system development process, formal methods are applied in a manner that best uses their capabilities.

The safety argument manager, SAM, is a tool to support the process of developing safety cases (Fodder, J. et al., see Proc. Safety-Critical Systems Symposium, Bristol, 1993). In SAM a safety case is expressed by a goal structure and associated solutions. Each solution is expressed in Toulmin argument form (1984). Fault trees can be constructed and attached to a goal. We have constructed the tool SAM, and investigated how these three different notations can be used in developing a real safety case for a complex system by completing a safety case study. This paper presents the case study, using SAM, of the PES (Programmable Electronic Systems) example (PES-programmable electronic systems in safety related applications, Health and Safety Executive, p.80-99, 1987).

As model-based formal methods (e.g. VDM, Z) are becoming popular for the development of safety-critical and complex systems in industry, automatic transformation from formal specifications to programs is an ideal and efficient approach to software production. However, it is impossible in general for this transformation to be fully automatic, because the language of first order logic used for specification is not decidable. This paper uses VDM (Vienna Development Method) as an example to investigate this difficulty, and proposes an approach to address the problem. Rules for automatically transforming abstract level VDM specifications are described and further transformation at a detailed level is discussed. Finally, further work towards the construction of a rule-based software system to support the transformation from VDM specifications to programs in general is addressed.

Software development using formal methods is believed to be a process of successive refinements from abstract specifications into concrete specifications. Refinement rules may be used to demonstrate that the concrete specifications satisfy the corresponding abstract ones. However, there are serious limitations of the refinement rules in both theory and in practical applications. This paper first uses examples to demonstrate the limitations, and then proposes a new software development model for improvement based on our experience. The limitations include (1) the refinement rules are not sufficient to guarantee that a refined specification (or concrete specification) satisfy the user's real requirements if it satisfies the abstract specification, (2) the existing refinement rules are not always applicable in theory during the successive refinements, and (3) the refinement rules are difficult to apply effectively in practice, due to various kinds of uncertainties and resource constraints. The proposed model suggests that system development using formal methods should be divided into two phases: a static development phase and a dynamic development phase, the whole process in each phase phase involving requirements analysis. In order to suit the new model, the existing refinement rules are modified.

There is a growing disappointment that formal methods have not been widely adopted in industry. One reason for this is that their application consumes prohibitive amounts of resource. Much research on the integration of available formal methods (e.g. Z, VDM, B-Method) and other structured methodology or object-oriented methodology have been conducted in order to make formal methods more practicable but its success has been very limited. However, little effort has been made to integrate properly formal methods, structured methodologies and object-oriented methodologies in order to take advantage of the desirable features of the three approaches. As an approach to the solution of these problems, we propose a language called SOFL (Structured-Object-Oriented-Formal Language) for system development. It supports the concept that a system be constructed using the structured methodology in the early stages of its development, and using object-oriented methodology at later, more detailed, levels. During the complete system development process, formal methods are applied in a manner that demonstrates their practicability. We first present the SOFL methodology (i.e. the methodology which SOFL supports), and then define the language SOFL by giving its abstract syntax together with an informal semantics. An example of developing a training centre system is used to demonstrate the usability of SOFL. Finally, future research on SOFL is briefly discussed.