China
Africa
Explore chapters and articles related to this topic
Modeling Guidelines of FreeRTOS in Event-B
Published in Ibrahiem M. M. El Emary, Anna Brzozowska, Shaping the Future of ICT, 2017
Eman H. Alkhammash, Michael J. Butler, Corina Cristea
Event-B [1] is a formal method that uses set theory and first-order logic to provide a formal notation for the creation of models of discrete systems and the undertaking of several refinement steps. In the refinement steps, the models represent different abstraction levels of system design. The consistency between the refined models in Event-B is verified through a set of mathematical proof obligations expressing that it is a correct refinement of its abstraction. The complexity in the design process is managed by abstraction and refinement. Refinement allows for postponing the introduction of some system features to later refinement steps. Rodin [2,3] is a tool used in the development of Event-B models. Rodin improves the quality of models through many features such as the identification of errors, the identification of required invariants, and proofs of consistency.
R
Published in Phillip A. Laplante, Dictionary of Computer Science, Engineering, and Technology, 2017
refinement-specification process by which a specification is refined by adding details and verifying the consistency of the previous specification with the new one. This approach is typical of denotational/descriptive languages and models.
Creating Formal Models from Informal Design Artefacts
Published in International Journal of Human–Computer Interaction, 2023
Judy Bowen, Benjamin Weyers, Bowen Liu
The final example we give of using the predicates is as a form of refinement. The goal here is to demonstrate formally that the two specifications (behavioural and Z) are consistent. Refinement and refinement algebra are used to transform formal specifications (which are typically abstract) into more concrete representations (Derrick & Boiten, 2001). While the ultimate goal may be an implemented system, refinement is equally well-used in considering specifications of the system at different levels of abstraction. In this way it enables us to understand whether or not two representations of the same system can be considered equivalent (or consistent).
Exploratory reconstructability analysis of accident TBI data
Published in International Journal of General Systems, 2018
Martin Zwick, Nancy Carney, Rosemary Nettleton
This analysis illustrates the type of results that can be obtained from exploratory modeling with RA and demonstrates the possibility of using RA to better understand – and potentially ultimately to improve – clinical outcomes. Analyses can be done at three different levels of refinement. Models are conceptually transparent, being simply conditional probability distributions of a DV given the states of IV predictors. The distributions can be readily summarized with easily interpretable decision trees.
Selecting spare parts suitable for additive manufacturing: a design science approach
Published in Production Planning & Control, 2021
Atanu Chaudhuri, Hasse Andreas Gerlich, Jayanth Jayaram, Abhijeet Ghadge, Johan Shack, Benjamin Hvidberg Brix, Lau Holst Hoffbeck, Nikolaj Ulriksen
Design science allows researchers to be actively engaged in problem solving, while still developing scientific contributions. The basic idea of design science research is that new generic designs will have significant practical relevance. Knowledge accumulation may be easier to crystallise and realise using a design science approach, with its focus on improving the extant generic designs (van Aken, Chandrasekaran, and Halman 2016). While both action research and design science involve active problem solving by the researchers, action research does not explicitly result in an ‘artefact’ as compared to a design science approach (Holmström, Ketokivi, and Hameri 2009). Design science follows the following four phases: (1) solution incubation; (2) solution refinement; (3) explanation through substantive theory; and, (4) explanation through formal theory. Solution incubation starts with understanding the problem and developing the first solution design, which is detailed enough to be implemented but may be incomplete. Solution refinement includes refinement of the initial solution design through iterations and to verify what works and what does not and, thus, includes design improvements, implementation and evaluation. This phase may also involve addressing unintended consequences. To proceed beyond problem solving, the researcher tries to evaluate the developed artefact from a theoretical point of view and focuses on development of a substantive theory which is a context-dependent theory developed for a narrowly defined context and empirical application. The final phase involves development of a formal theory, if possible, which is aimed at broader generalizability (Holmström, Ketokivi, and Hameri 2009). As the objective of this research is to solve a problem faced by the company by developing a process or an artefact and to generalise the findings for a theoretical contribution, we adopted a design science approach.