China
Africa
Explore chapters and articles related to this topic
Design in Action: From Prototyping by Demonstration to Cooperative Prototyping
Published in Joan Greenbaum, Morten Kyng, Design at Work, 2020
The main purpose of executable specification approaches is to obtain a full, formal specification of what (parts of) the future system should do. The specifications are made in a formal, executable specification language, meaning that a program, and thus a prototype, can be generated automatically from the specification. Although in theory, users and designers can evaluate the specification by evaluating this prototype, in practice this is hardly ever done. The specification languages that serve as basis for generating the prototypes are usually not suitable as a means for communication with users and empirically it has turned out that a full-scale formal specification of a system requires an effort similar to traditional programming of the system. Offsprings of these two approaches are seen in the so-called CASE-tools. Code generating CASE-tools have, however, not been used enough yet to assess their ability to support prototyping.
Fundamentals of Systems Engineering
Published in Julio Sanchez, Maria P. Canton, Software Solutions for Engineers and Scientists, 2018
Julio Sanchez, Maria P. Canton
Some authors distinguish between degrees of rigor. The highest degree, called formality, requires that development be made strictly according to laws of mathematics and logic. In this sense formality is a high degree of rigor. One field in which the issue of rigor and formality gain particular importance is in software specifications. A logical formalism has been developed which allows the precise specification of software. The mathematical expressions, usually based on the predicate calculus, allow the representation of complete programs, or of program fragments, in symbolic expressions that can be manipulated according to mathematical laws. Some of the advantages of this methodology claimed by it advocates are the following: Formal methods allow the software engineer to specify, develop, and verify a software system using a formal specification language so that its correctness can be assessed systematically.They provide a mechanism for the elimination of program ambiguity and inconsistency through mathematical analysis, thereby discovering errors that could otherwise go undetected.They allow a software problem to be expressed in terms of an algebraic derivation, thus forcing the specifier to think in more rigorous terms.These methods will eventually make possible the mechanization of programming thereby revolutionizing software development.
Systematic Derivation and Evaluation of Domain-Specific and Implementation-Independent Software Architectures
Published in Roger H.L. Chiang, Keng Siau, Bill C. Hardgrave, Systems Analysis and Design, 2017
K. Suzanne Barber, Thomas Graser
Formal specification languages and their associated analyzers (e.g., Alloy and its accompanying tool ALCOA) provide a means for specifying requirements in precise terms and conducting computer-based analysis to ensure correctness based on well-defined properties (Jackson, 2006). However, using a formal specification language requires a level of discipline and rigor when gathering and representing stakeholder requirements in order to map requirements to the constructs of the chosen language and interpret evaluation results in terms of which requirements will and will not be satisfied.
Algebra for Enterprise Ontology: towards analysis and synthesis of enterprise models
Published in Enterprise Information Systems, 2018
Z notation was developed by the Programming Research Group (PRG) at Oxford University. It specifies software systems in the form of a formal specification language. It offers a package of reusable pre-defined types (e.g., set, sequences, relations, functions) and defines operations by specifying pre- and post-states. One of the benefits gained by using Z notation is the reduction in complexity due to large specifications and the improvement in the readability and manageability. In exchange for this advantage, Z notation introduces a new challenge: the authors have to fit DEMO specifications into the predefined types and patterns of Z notation. Moreover, even though Z notation is commonly adopted for formalizing models, there seem to be no existing attempts to investigate algebraic operations in it as addressed in (Moreira et al. 2004). Thus, Z notation was not chosen for this study.
DevFemOps: enhancing maintainability based on microservices using formal engineering methods
Published in Connection Science, 2022
Tetsuo Fukuzaki, Shaoying Liu, Michael Butler
In software development, formal methods are one of the techniques to improve the quality of software development. Formal methods consist of formal specification descriptions and formal proofs. Formal specification descriptions use set theory and logic to describe software specifications, so that functional requirements can be described without ambiguity. First, we can write a formal specification with a high level of abstraction, and then increase the explicitness of the specification through a process of refinement. Formal proofs are used to guarantee that there are no contradictions in the specifications at a certain stage, and that the refinement process has been carried out correctly.