The rapid development of machine learning (ML) systems has raised many concerns over their quality.Due to the inherent complexity and uncertainty, most of the traditional quality assurance techniques have been challenged, including requirements specification.Current strategies mainly focus on model extraction from existing neural networks to improve interpretability and facilitate system analysis, but failing to include user expectations on the system.To handle the problem, this paper proposes a specification framework for ML requirements where each ML system is regarded as a set of snapshot systems along the evolvement process.There are 3 layers in the framework and the hierarchy indicates that higher-level models need to be built based on lower-level ones.The bottom layer consists of meta snapshot model and meta data model serving as the meta models for snapshot systems and data requirements respectively.The middle layer is for snapshot models each describing a snapshot system through relations between its outputs produced with different inputs.The top layer is a learning model capturing the evolvement process by transitions among snapshot models.These transitions are activated by data models instantiated from meta data model.We adopt the specification of a self-driving system to illustrate the framework.

Software Product Line deals with the development of product families for diverse market needs and includes feature model to describe the structure of the included products. Since feature model is lack of detailed specification of individual features, some behavior-oriented methods have been proposed to analyze the inner functionalities of features. But how these functions relate to the feature model remains a problem and a systematic approach is still needed to support the whole process of product family modeling. This paper provides a formal engineering approach to modeling product family where feature model evolves as individual features are formalized through informal, semi-formal and formal stages. For each stage, a set of evolvement rules are given to guide the refactoring of the feature model which will then serve as a basis for formal specifications of individual features. Such an iterative process repeats until achieving a feature model with consistent feature specifications. A case study is described to illustrate the effectiveness of our approach.

Although formal specification is considered as a potential technique for improving the accuracy of requirements documentation and the quality of software product, the difficulty of using formal notations leads to the gap between this technique and the practice of software development. Many approaches for solving this problem were proposed. Most of them provide automatic transformation from informal requirements into formal specifications. However, rather than clarifying and formalizing requirements on the semantic level, they only use syntactic rules to translate between different languages. To handle the challenge, this paper describes an approach for formal specification construction based on pattern knowledge. The knowledge is composed of a set of inter-related specification patterns. Each pattern defines the method for formalizing one kind of function, including derivation knowledge for guiding the clarification of the function and transformation knowledge for formally representing the clarified function. A supporting tool is also described in the paper which derives necessary function details of the intended requirement through interactions by applying the derivation knowledge and transforms these details into formal specifications by applying the transformation knowledge. An experiment on the tool is held and the result shows that the tool can help formalize requirements efficiently and enhance the quality of the resultant formal specifications.

Service-based software (SBS) modeling is considered as a promising way to develop high-quality service-based systems. One major challenge of this methodology 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. In this paper, we propose an evolutionary method for the formal specification construction of SBS to tackle this problem. Initial requirements are gradually transformed into a formal design specification through three steps during which existing services are discovered, filtered, selected and adopted. Candidate services are discovered through a keyword-based searching. Then the services are analyzed from both the structural and behavioral perspectives for filtering. A specification-based testing technique is exploited to rigorously determine which candidate services are finally selected. The selected services are incorporated into the formal design model of the system. We present a case study that was conducted for evaluating the usability of the method. We have also developed a prototype tool for supporting the method to be applied in practice.

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.

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.