Antilock Braking System (ABS) is one of the most critical systems in the context of vehicles' mechatronics. The main purpose of the ABS system is allowing the wheels to stop while preventing sliding. It is responsible for ensuring a secure stopping of the vehicle, a very critical factor in trip safety. Therefore, the process of its construction should be performed with high care, and this is why theoretical modeling is highly needed. In order to help engineers to develop and study such a critical system, we propose a standard model that includes the essence of Antilock Braking System using a formal method called Event-B. This model may be used to reveal some bugs during proving that may go otherwise undetected. At the same time, the model can be animated to observe the system behavior.
TopIntroduction
The Antilock Braking system is an active safety system that aims to reduce the number of road accidents (Cao, Chen, & Zhou, 2018; Voevodin et al., 2018). ABS is an electronically controlled system that allows the driver to keep up control of the vehicle amid crisis braking while at the same time keeping the wheels under control. Besides, by keeping brake weight just underneath the point of making a wheel lock up, ABS guarantees that the most extreme braking power is utilized to stop the vehicle while minimizing the braking distance as much as possible (Mammosser, Boisveert, & Micheau, 2013). In an ordinary ABS, the measure of the angular velocity of the wheels and the linear acceleration are done by means of sensors. These data received from these sensors are utilized to settle on the choice, regardless of whether the wheel is going to lock up. If a tendency toward wheel block is occurred, the brake cylinder pressure is reduced. As soon as the wheels disallowed from locking, the pressure will increase again.
The ABS system is very critical in the road security domain, thus its design of should be proceed carefully. Therefore, we used one of most sophisticated techniques in system design that are formal methods (Adamiec, Dziubiński, Siemionek, & Drozd, 2018). Formal methods are rigorous computer techniques that allow, with the help of specialized languages and logical rules, to ensure (ideally) that there is no lack of computer programs - which is particularly important when they involve human lives - software or mathematical demonstrations. By using this kind of method, we can improve our understanding of the system behavior and at the same time detect ambiguities, incompleteness as well as inconsistencies. In this paper, we use The Event-B formal method that adopts a mathematical notation based on set theory. Furthermore, Event-B use refinement to represent systems at different abstraction levels which facilitate system design (Jarrar & Balouki, 2018; Debbeh, Bon, & Collart-Dutilleul, 2019). It includes mathematical proofs that allow the verification of consistency between abstraction levels and the preservation of invariants (Ondruš & Kolla, 2018). This method has been effectively used in different systems where not bugs were detected. For instance, the driverless meteor in Paris worked correctly and no bugs were identified after the theoretical proofs, neither at the functional approval. This achievement encourages Alstom and Siemens Transportation Systems to use this method to develop future metros. Therefore, we also used Event-B to develop a standard antilock braking system model.
The main contribution of this paper is providing a sort of a standard model of the ABS system. This model is suitable for any ABS systems regardless of the technologies and techniques used during fabrication which enlarge its use to almost all ABS systems. It includes the essence of ABS and can be used as a first abstract model; afterward it can be refined by adding more typical requirement and parameters of the studied system. Alongside the development and refinement of models, proof obligations ensure the consistency and absence of failure in the system which highly guarantees the correctness of the system.
The rest of the paper is structured as follows. Section 2 gives some background on related works, ABS, and the used method. In section 3, we present the set of requirements considered in this paper. The main content of the paper is in Section 4 describing our approach to develop the ABS. Section 5 concludes the paper.