Related Experiment Video
Updated: Mar 18, 2026
08:05
Design and Analysis for Fall Detection System Simplification
Published on: April 6, 2020
11.2K
Formal analysis of imprecise system requirements with Event-B
Hong Anh Le1, Shin Nakajima2, Ninh Thuan Truong3
1Hanoi University of Mining and Geology, Bac Tu Liem, Hanoi, Vietnam.
Springerplus
|July 12, 2016
Summary
This study introduces a new method for formally analyzing imprecise system requirements using Fuzzy If-Then rules and Event-B refinement. This approach enables precise verification of functional properties for complex systems.
Area of Science:
- Computer Science
- Software Engineering
- Formal Methods
Background:
- Formal analysis of system requirements demands precision, yet stakeholders often use ambiguous or fuzzy terms.
- Existing methods for representing imprecise requirements with Fuzzy If-Then rules lack robust verification techniques.
Purpose of the Study:
- To propose a refinement-based modeling approach for the specification and verification of imprecise system requirements.
- To bridge the gap between fuzzy requirement representation and formal verification.
Main Methods:
- Representing imprecise requirements using set theory.
- Translating Fuzzy If-Then rules into Event-B notations via refinement.
- Utilizing the RODIN/Event-B platform for property verification.
Main Results:
- A novel method for modeling and verifying imprecise system requirements is presented.
- Demonstrated the verification of both safety and eventuality properties.
- Successfully applied the method to the Crane Controller example.
Conclusions:
- The proposed refinement-based approach effectively handles imprecise system requirements.
- Formal verification of functional properties for fuzzy requirements is achievable using Event-B.
- This method enhances the reliability and precision of system requirement analysis.
Related Concept Videos
01:15Assumptions of Survival Analysis
475
Survival models analyze the time until one or more events occur, such as death in biological organisms or failure in mechanical systems. These models are widely used across fields like medicine, biology, engineering, and public health to study time-to-event phenomena. To ensure accurate results, survival analysis relies on key assumptions and careful study design.
475
01:27The Precise Definition of a Limit
390
Understanding the formal definition of a limit is essential for precise mathematical analysis. This concept allows us to rigorously determine how a function behaves near a particular point without relying on ambiguous notions such as "getting close." The ε-δ definition plays a foundational role in calculus, ensuring analytical clarity and logical consistency in limit evaluation.The formal definition states that the limit of a function f(x) as x approaches a is L, written asif for...
390
01:10Propagation of Uncertainty from Systematic Error
1.6K
The atomic mass of an element varies due to the relative ratio of its isotopes. A sample's relative proportion of oxygen isotopes influences its average atomic mass. For instance, if we were to measure the atomic mass of oxygen from a sample, the mass would be a weighted average of the isotopic masses of oxygen in that sample. Since a single sample is not likely to perfectly reflect the true atomic mass of oxygen for all the molecules of oxygen on Earth, the mass we obtain from this...
1.6K
01:26Constraints and Statical Determinacy
1.1K
In structural engineering, the equilibrium of a system is not only determined by its equations of equilibrium but also with the help of constraints. Constraints refer to restrictions on the motion of a system. The proper combinations of constraints can minimize the total number of constraints needed to maintain a system in mechanical equilibrium. When this happens, the system is said to be statically determinate. For such systems, the unknown reaction supports can be estimated using equilibrium...
1.1K
01:27State Space Representation
668
The frequency-domain technique, commonly used in analyzing and designing feedback control systems, is effective for linear, time-invariant systems. However, it falls short when dealing with nonlinear, time-varying, and multiple-input multiple-output systems. The time-domain or state-space approach addresses these limitations by utilizing state variables to construct simultaneous, first-order differential equations, known as state equations, for an nth-order system.
Consider an RLC circuit, a...
Consider an RLC circuit, a...
668
01:16SFG Algebra
366
In Signal Flow Graph (SFG) algebra, the value a node represents is determined by the sum of all signals entering that node. This summed value is then transmitted through every branch leaving the node, making the SFG a powerful tool for visualizing and analyzing control systems.
Each node in an SFG corresponds to a variable, and the interactions between nodes are represented by branches with associated gains. When multiple branches lead into a node, the value at that node is the sum of the...
Each node in an SFG corresponds to a variable, and the interactions between nodes are represented by branches with associated gains. When multiple branches lead into a node, the value at that node is the sum of the...
366