Modeling from the demand model from a lightweight formulation method
- Case Study of the MIS system to specification with the RADL language
Summary formulation method for improving the correctness of the software, the reliability is significant, which can greatly reduce the post-maintenance cost of software, but due to the design cycle and the quality of personnel, the formal method has not been widely used. This paper introduces a new software development method - a lightweight formulation method, from the perspective of theory, its cause and basic idea, and give a lightweight formulation method in MIS system analysis from the perspective of practice Application examples.
Keyword lightweight formal method requirements Modeling software engineering
I. Introduction
With the continuous growth of software system complexity, especially software applications in cutting-edge, it makes it a very important issue for development security and reliable software. Traditional software engineering methods have developed a series of principles, standards, and steps to improve software productivity and quality in different aspects and extent. However, software system needs generally use natural language and pseudo code as a description language. Due to the defects such as secondary and inconsistency, the pseudo code is too much attention to achieving details, making the description and construction process of software systems often hide. A large number of errors, and these mistakes cannot be solved only by testing. For industries that require high security and high reliability, such as nuclear power plants, aerospace, rail transportation, etc., this problem is particularly important, must have a systematic approach to solve. It is not negligible to general application systems, security and reliability.
The formal method is a mathematical method, which can clearly, accurate, abstract, concise, and verify the software system and its nature, and greatly improve software security and reliability. Many formulated methodologists have studied the problems of formulation and their development trends, pointing out that the formal method is not universal, the current formal research and practice level still does not exert the potential of formulation methods [HALL 1990, Browen 1995].
In academic and engineering, there is still a considerable difficulty in the application of formulation methods, such as longer design cycles and high personnel quality, which makes it unfair to completely formally formulating the entire development process at present stages. . In order to make the formal method more practical, more economical, it is suitable for the requirements of system development in different fields, and formal research workers have begun to explore a new software form development method - lightweight formal method, It is focused on selectively formulating some stages or in certain portions of software development. This paper explains the causes and basic idea of lightweight formulation methods, and then uses the RADL (Recurrence_Based Algorithm Design Language) to give a lightweight formulation specification description of partial requirements in a MIS system.
Lightweight formulation method in two demand analysis
In the history of formulation, due to the early practice of high security, high-risk industries, in order to ensure the safety and reliability of the system, a strict and complex process is often used. This causes longer design cycles and high personnel quality when constructing a complete formal system model. Practice has proved that the complete formal formation of the entire system is extremely difficult at this stage.
In order to make the formal method more practical, more economical, and formalized research workers have begun to explore lightweight formulation methods, the purpose is to give up the limited resources, limited construction, limited interaction, frequent management, reliability requirements, Some specification verification mechanisms can also avoid critical defects. Basic thinking is to cut the original "heavy" formal method, which will be applied to a certain stage or some part of software development, thereby effectively balancing the contradiction between software quality and productivity. At this stage, lightweight formulation has some attempts in aerospace, embedded development, voice communication, component development, and other industrial applications [Easterbrook 1997, 1998, HORL 2000, Matsumoto 2002, Murray 2001].
Daniel Jackson [Jackson 1996] believes that the lightweight formulation method focuses on observation from different angles, and has selected formal technology. In the standardized language, traditional formal methods often contain a large number of mathematical symbols, and the normative language is regarded as a general mathematical representation, which hinders the formal method in general. Applications in system development, lightweight formal method advocate language and their aids. In the relationship between testing and prove, the lightweight formulation method waited for the correctness of the prove, and the fundamental problem of testing did not explain that the system was unlikely, but found that the mistakes were not found. Mode of MODEL CHECKING successful application in some areas is better examples. The lightweight formulation method also advocates that the large system is selectively adopted, and the different sections are combined together on the basis of consistency. In terms of specific implementation, there are also some results, such as in the construction of demand regulations, Steve EasterBrook [EasterBrook 1997] summarizes the research results of the application of lightweight formulation methods in the NASA project, divided into four processes that form demand specifications. Steps: (1) describe the demand in clear, precise, and no sense.
(2) Confirm and correct the inconsistency within the specification.
(3) Test demand based on system expected behavior.
(4) Feed back the test results to the author of the demand.
The current software system is often extremely complex, understanding and description of the nature of the problem. During the demand process, there is often a lot of inconsistency and erroneous errors, and the more the error is found, the higher the cost of repairing the wrong mistake [ZHOU 2001]. Formalized descriptions have precise semantic and reasoning capabilities, and improve the clarity and accuracy of demand specifications by no means description, consistency check, type check, validity check, behavioral detection, seeking examination, etc., can improve the clarity and accuracy of demand specifications, and early Discover the specifications and design defects hidden in the demand, and eliminate the production of large partial errors in the initial period of system construction. Therefore, the idea of using lightweight formulation methods, this paper is an attempt to introduce formal methods in the demand modeling stage of MIS system development.
3 lightweight formulation method in the MIS system
Lightweight formulation methods currently stay in high reliability, high security industries. As an attempt, we applied a lightweight formulation, with RADL as a description language, the system requirements of a MIS system are specified.
3.1 Introduction to RADL
The RADL language is a class-based algorithm design language that Xue Jinyun is defined by a PAR method that implements an algorithm procedure and semi-automated PAR method is an important part of the PAR method. Current PAR method and its RADL language are mainly applicable to the development of Safety-critical software components. [Xue 1998]
The original intention of the RADL language is designed for the development of algorithm procedures in computer programming. However, as a strict definition formal language, RADL also thinks about various aspects of software system design, such as describing software systems and their behavioral patterns, portraying software systems, application, comparison, and conversion, software tools Development. Therefore, it can be regarded as a broad spectrum language, which can be used to score the underlying design and describe the high layer abstraction. For the RADL language, the high-level description is actually a mathematical model of the establishment of a software system.
Therefore, we use the RADL language as a description language to a MIS system-Provincial Natural Science Fund Project Management System (NSFPM, Natural Science Finance Project Management System) - Demand Modeling.
3.2 Function Description
First give a problem description of NSFPM, ie requirements (Requirement).
NSFPM is a MIS system. First, the project applicant submits the application electronic document to the Fund Project Management Office. The project administrator then introduces the metadata in the application electronic document (record the key information related to the management related to management) into the system. The project administrator will then review experts for the application of the project to select the experts in the corresponding discipline. Experts returned to the review projects, and the project administrator scored the application project according to the opinion. Finally, the project administrator conducts a unified assessment of all projects according to the expert's overall rating, and the assessment results are submitted to the Fund Project Management Committee. The project administrator submits the final comments of the Fund Project Management Committee to the NSFPM system. Usually, project administrators also maintain information about experts. 3.3 System modeling
3.3.1 Domain Modeling
First, modeoforming, ie analysis is analyzed.
The first step in analysis is to point out what the system can be used, who will use it. All use cases must begin with a role (actor), and some use cases have also ended in the role. The role is a person or other system located outside the working system. [Cockburn 2001]
The roles involved in this system include project administrators, project applicants, experts. Project applicants are not directly and system interaction, and the function of submitting the application project is executed by the project administrator. Experts are not directly interacting with the system, and the function of the application project score is executed by the project administrator.
Therefore, this system is managed as the core, and the project administrator is the main character color, obtaining a concise case:
Project Management includes import projects, editing projects (selected review experts, entry expert ratings, changing project status), and evaluation projects.
Project maintenance includes deleting a project, retrieving items, viewing items, browsing documents, and modifying documents.
Expert maintenance includes registered experts, cancellation experts, modification experts, view experts, increase experts, and delete experts.
The results of the NSFPM system analysis are in the case of the UML, as shown in Figure 1.
Figure 1: Role and use cases of NSFPM systems.
3.3.2 System Modeling
Then, transfer from the domain modeling to the system modeling. The following is a concise UML class diagram of the system key model. It should be noted that in order to describe the problem, we do not use the GET () method in the implementation to ensure that the data is hidden, but set the attributes of the class to public properties to directly access.
Figure 2: Simplified class diagram of the NSFPM system.
According to the above discussion of the example and class diagrams, we introduce the following abbreviations, using the same types as the same description, and variables (if needed, you can use x1, x2 ...) to simplify the description of the model.
Types of
variable
Project P
ProjectBase PB Expert (expert) E Expertbasr (Expert Library) EB Edoc (Electronic Application) ED Project_expert (association of project and expert) PE
3.4 Formal Description
We are defined in the state definition and behavior specification in the needs model. Here are some examples.
3.4.1 Formal State Definition
For each type with status model, we must be able to distinguish between different attributes of the type (in practice, state definitions to guide our refine status model, especially those like properties). This article is defined as an example as an example in the Project state, and "onjudging" and "onjudging".
Application
/ / The project is in the application status, meaning //p.status = onapplying Implies
Begin
// There is a project code //
P.PID ≠ Null
// Applicant must not exceed two items in the research project //
AND σ (p1: p1∈pb ∧ p1.AID = P.AID ∧ p1.status = onstudying: 1) ≤ 2
// Applicant does not have a project // /
And p1∈pb ∧ p1.AID = P.AID ∧ p1.status = onstudying ∧ p1.whenfinished End In evaluation // The project is in the state, meaning // p.status = onstudying Implies Begin // There is a project score // P.Score ≠ Null // Project score in this discipline in the top ten /// AND σ (p1: p1∈pb ∧ p1.sid = p.SID ∧P1.score> P.SCORE: 1) <10 End 3.4.2 Formalized behavior specification Here are some behavioral specifications. Each behavior has an identifier, front assertion and rear assertion. This article is configured as an example in which two types of "importProject) and" Select Expert "(Select Expert) in NSFPM are used as an example. Import item // Import an electronic application book // NSFPM :: ImportProject (ED: EDOC) AQ: // There is no items with the content of the electronic application content in the project library. Ed.Key = p.key ∧ ~ pb.search (p) Ar: / / Generate project code // P.PID ≠ Null // Project status is "Apply" or "elimination" // And p.status = onapplying ∨ p.status = Onlost Choose an expert / / For project selection review experts // NSFPM :: SELECTEXPERT (P: Project, E: EXPERT) AQ: // Project exists, the project status is "application" // Pb.Search (P) ∧ p.status = onapplying // Expert existence, expert status is "registration" // And Eb.Search (e) ∧ E.status = ONLOGIN // Project disciplines and expert disciplines /// And P.SID = E.SID // The project has been less than 5 /////////// And pe.pid = p.PID ∧ pe.getnumberofexpert () <5 // Auxiliary variable x, record the number of experts in the current project /// And aux x = pe.getnumberofexpert () Ar: // Project is an expert increasing 1 //// pe.getnumberofexpert () = x 1 // Project expert association has increased expert // And pe.search (E.ID) The specifications defined above are used as a description of the program status and behavior. It is used in our NSPFM system development to determine if the system is operating normally. This further ensures the clarity, correctness, and reliability of the system. Summary and discussion In the process of constructing the above MIS system configuration, we focus on the key steps of system development - demand analysis, apply formal methods to demand modeling, without pursuing full form, to achieve lightweight objectives, At the same time, the system's clarity, correctness, and reliability are guaranteed, and the development cost of the system is reduced. The application of lightweight formulation methods remains to be further studied in various stages of system development. After modeling the needs of demand, how to evolve and refine existing specifications in subsequent phases have become the goal of further research. Finally, a sentence with Dianel Jackson concludes. Compared to traditional formal methods, lightweight formulations also have gaps in the expression capability and application, as well as the laser used in medical treatment, compared to ordinary lamps, it is weak, coverage smaller However, but its efficiency is higher, the effect is more remarkable. main reference [Beck 2001] Kent Beck. Analyze limit programming - hug changes. Translation of Tang Dongming. People Post Press. Wendy Boggs & Michael Boggs. Mastering Uml with Rational Rose 2002. Translation of Qiu Zhongpan. Electronic Industry Press. [Boiten 1992] E.A.BOITEN ET AL. HOW to Produce Correct Software - An Introduce To Formal Specification and Program Development by Transformation. The Computer Journal, Vol.35, No.6. [Brooks 1995] Frederick Brooks. The Mythical Man-Month. Wang Yinglation. Addison Wesley 1995. [Browen 1995] Jonathan P. browen. Seven More Myths of Formal Methods. IEEE COMPUTER, JULY. [Cockburn 2001] Alistair Cockburn. Write a valid use case. Wang Lei, Zhang Li. Machinery Industry Press. [Craigen 1995] D. CraiGen et al .. Formal Methods Reality Check: Industrial Usage. IEEE TRANS. Soft. ENGI., VOL. 21, NO. Steve Easterbrook et al. Formal Methods for verification and validation of partial specifications. NASA-IVV, NO.10. [Easterbrook 1998] Steve Easterbrook et al. Experiences Using Lightweight Formal Methods for Requirement Modeling. IEEE TRANS. Soft. ENGI., VOL.24, NO.1. [Fowler 2000] Martin Fowler, Kendall Scott. UML is essential. Translation of Xu Jiafu. Addison Wesley 2000. [Hall 1990] j.a.hall. Seven Myths of Formal Methods. IEEE Software, September. [HORL 2000] Johann Horl et al. Validating Voice Communication Requirements Using Lightweight Formal Methods. IEEE Software, Vol.17, No.3. [Jackson 1996] Daniel Jackson & Jeannette Wing. Lightweight formal methods. [Jacobson 2000] Ivar Jacobson et al. Unified software development method. Zhou Bosheng et al. [Mitchell] rechard mitchell. Analysis in the contract - Recorder case study. Translation of Zhen Lei. Michihiro Matsumoto. Lightweight Formal Methods for Component-Based Software Developments. CARROLL MORGAN. Programming from specification. Zongyan translated. Machinery Industry Press. Leesa Murray. Lightweight Formal Methods for Embedded Software. Of Rational 2001] Rational. Rational Unified Process 2000. Rational Software Corporation 2001. [Sobel 2002] Kelley Sobel et al. Formal Methods Application: An Empirical Tale of Software Developments. IEEE TRANS. Soft. ENGI., VOL.28, NO32. Bruce E. Wampler. Java and UML object-oriented programming. Translation of Wang Haipei. People Post Press. Xu Zhengwen. How to investigate and analyze system needs. China Computer News, August. Xue Jinyun (Xue Jin Yun). FORMAL DERIVATIONOF Graph Algorithmic Programs Using Partition-And-Recur. J. OF Comput. Sci. & Technol, Vol.13 No.6. Zheng Hongjun, Zhang Nai Xiao. Formal method in software development. Zhou Ziying. Modern software engineering (medium). Science Press, 2001.
