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.
Building trust of Blockchain-based Internet-of-Thing services using public key infrastructure
Published in Enterprise Information Systems, 2022
Wattana Viriyasitavat, Li Da Xu, Assadaporn Sapsomboon, Gaurav Dhiman, Danupol Hoonsopon
A BIoT service to be used by a user is evaluated based on user’s requirements. One example of the requirements can state that a BIoT service shall use permissioned Blockchain with PBFT, or another requirement can specifically state that the validators in running PBFT must be from USA and China. The compliance of these requirements reflects trust of that BIoT service, and trust is subjective in the viewpoint of different users. Specification language serves as a formal tool to encapsulate the requirements (Viriyasitavat, Da Xu, and Martin 2012), which becomes a fundamental ground for automatic compliance checking (Viriyasitavat, Da Xu, and Viriyasitavat 2014).
Creating Formal Models from Informal Design Artefacts
Published in International Journal of Human–Computer Interaction, 2023
Judy Bowen, Benjamin Weyers, Bowen Liu
In our examples we use the Z specification language, but the same approach can be used with any similar declarative specification languages. A typical Z specification consists of declarations and definitions of required types, a description of the system being modelled in terms of its observable components (the observations) and descriptions of operations that can be performed on the system. Z uses a notation consisting of schemas which can be visually constructed into schema boxes which are collections of state observations and values. The system is described in a state schema as follows: