—The cost of ﬁxing software requirements errors after deployment is so high that it is vital to come up with ways to ﬁnd and ﬁx requirements errors early in the life-cycle of a project. The work in this paper advocates for the use of formal methods as an alternative approach to guarantee the correctness of the software from requirements to code. We present a formal-methods based approach for the early validation of functional requirements. Our approach relies on formal methods techniques such as program reﬁnement, correctness-by-construction (CbyC), and automated code generation. We present two case studies that showcase our approach; for the case studies, we discuss design decisions, ﬂaws encountered, and lessons learned. Index Terms —Event-B, Formal Methods, Formal Speciﬁca- tions, Software Requirements, Veriﬁcation. I. I NTRODUCTION Software errors result in signiﬁcant costs, schedule overruns [11], [10], [3], [4], quality issues, and failures to deliver the speciﬁed functionality. While there have been various techniques to enhance requirements analysis and detection of software defects, software products are shipped with various defects that are rooted in the requirements. Such problems are exacerbated in the presence of safety-critical, autonomous, and mission-centric systems. We present a novel approach to validate software require- ments in the early phases of software development with the EVENT B formal method [1]. We advocate for an approach that not only allows early validation of software requirements but also enables the accurate implementation of functional requirements. Early validation of software requirements seeks to reduce the high cost of ﬁxing bugs in later software development phases [4], [3]. Hence, we model the functional software requirements of the application in E VENT B, we reﬁne the model with the Rodin platform [2], and we use the E VENT B2J AVA code generator [12], [6] to generate a prototype implementation of it, and optionally unit-test the generated code. The generated code is not meant to be a ﬁnal implementation of the E VENT B model, but a code used for validation purposes only. We use two case studies to showcase our ideas on validation of software requirements and generation of source code for functional requirements. The ﬁrst case study is about the use of the E VENT B formal method and unit-testing techniques to validate the functional requirements of R OADFIGHTER , an Android car racing game. The second case study is about the validation of the software requirements of a chat system (similar to WhatsApp) fully in E VENT B, without resorting to the use of unit-testing.This paper is organized as follows: Section II presents our proposed approach for validating software requirements with EVENT B. Section III presents our ﬁrst case study, an Android car racing game. Section IV discusses our second case study, a chatting system. Section V discusses some work that relates to the validation of software requirements. Finally, section VI presents conclusions and discusses future work. II. T HEMETHODOLOGY Figure 1 presents our methodology to validate the functional software requirements of applications. Informal requirements are elicited as User Stories, which are then utilized to write a formal model of the system in E VENT B. The E VENT B model is reﬁned as required, and Proof Obligations are discharged along the way to ensure that the model is sound. We use the EVENT B2J AVA tool to generate a prototype implementation of the application. We manually write unit tests to validate the implementation of the application. The prototype is run, unit tested, and thus the software requirements validated. If a test fails, the informal or the formal speciﬁcation is evolved and the whole validation process is restarted. We encode informal requirements as User Stories, which are textual templates of the form “as a <Role>, I want to <Goal /Desire >so as to <Why>” that encode functional software requirements. Although User Stories are typical of Agile methodologies, we use them here as their syntax closely follows the syntax of E VENT B. A User Story includes some Acceptance Criteria against which it should be validated. An acceptance criterion has 3 components, a Given part that describes when the functionality may be triggered/executed (which depends on the internal state of the system), a When part that tells us when the functionality is to be executed (which depends on the user’s decision), and a Then part that describes how the state of the system changes when that functionality executes. III. R OADFIGHTER The goal of this case study is to demonstrate how reﬁnement calculus with E VENT B and unit testing techniques can be combined to sanitize and validate the functional software requirements of a car race Android app. R OADFIGHTER is a racing arcade game. The goal of the game is to reach the ﬁnish line without running out of time or hitting other cars. The car racing game consists of a single carcontrolled by the user, the car is placed on a lane that has a ﬁnish line andborders . Cars run over lanes. Several static and dynamic objects called obstacles as well as other artiﬁcially controlled Fig. 1. Chat: validation of software requirements cars called opponents are placed on the lane. The simulation of the physics involved in driving a car can be as accurate as the developers want and the hardware allows. A scoring system is modeled to reward players. As games are meant to attract people, variations of the scoring system and rules can be implemented in order to achieve market differentiation. Two important aspects of physics involved in artiﬁcially simulating a car race are kinetic movement and collision detection. A straight transformation of physics equations of accelerated movement into algorithms (implemented in Java for instance) is not possible because of their continuous nature. Game programmers often opt to apply a discrete approach based on Euler Discretization. The following equations model a uniformly accelerated movement. You may see that these equations are recursive, and require an initial value, similar to a state machine. Thus, tis the time step-value of the discrete system. acc(obj) =a vel(obj) =vel(obj) +acc(obj)t pos(obj) =pos(obj) +vel(obj)t A great diversity of algorithms exist to calculate collisions, which may use boxes, spheres or ellipses as their geometrical enclosing form to calculate the intersection of objects. Because exhaustive collision detection is time demanding, the trade-off thus is the speed of processing vs. exactitude [8]. We consid- ered a two-dimensional box collision detection algorithm as shown below. jposx(obj1)posx(obj2)j<width (obj1) 2+width (obj2) 2^ (1) jposy(obj1)posy(obj2)j<height (obj1) 2+height (obj2) 2(2) We enclose each object into a 2D box of width and height dimensions and then test if there is an intersection between the two. We use boxes in our car racing game, but circlesor ellipses might be the best choices for other scenarios with objects such as balls (Billiard game) or humans. A. The Event B Model Figure 2 shows R OADFIGHTER ’s E VENT B Model. Machine RoadFighter sees context ctxt 0(not shown here), which declares two carrier sets OBJECTs andLANES representing all the possible objects and race lanes in the game, respectively. Variables objects andlanes are the current objects of the game and the existing race lanes; obstacles is the set of static objects of the game, and cars is the set of dynamic objects. Every object has a horizontal and vertical position (posX and posY ), a total function that maps the object with an integer number representing the position. Objects are two-dimensional with a height and a width . Variables vel (velocity), acc (acceleration), and lean (bending from the straight-up position) keep track of the cars’ kinetic. Variable collided (a set) keeps track of the collided objects. The event update posupdates the car’s position according to Euler’s discrete movement approach, popular in real-time applications, where elapsed is a global measure of the time passed since the last update to the object’s position, expressed in milliseconds (converted to seconds in the model). Events may only be triggered when the guard (the where condi- tion) holds. The event update pos models an unbounded substitution in E VENT B (the any clause), so it allows the implementer of the event to choose any value for carand elapsed that veriﬁes the guard. The symbol “ :=” represents simple assignments in E VENT B,?the empty set, and !a total function. B. Unit Testing We wrote 29 JUnit tests to check the absence of errors in code. As E VENT B2J AVA translates each event into an independent Java class, we used each unit test to check the functionality of each event. When a test failed, we checked the code of the respective event in the Rodin platform, made the respective changes, and generated code again. All the tests passed at the end. The JUnit test below checks that the delete car event properly deletes a car that has previously been created. The way events are structured allows us to write unit tests easily. The car object needs to be given proper initial values following the respective event guard in order for the object to be added to the list of cars. E VENT B2J AVA generates two Java methods for each event, a “guard” method that checks if the event guard holds, and a “run” method that executes the event body in case its guard holds. If the test fails, likely, the guard did not hold initially thus the event body did not execute. @Test public void delete_car() { // initial values for Car, Desc, H, etc. ADD_CAR ac = new ADD_CAR(machine); ac.run_ADD_CAR(Car,Desc,H,W,X,Y,F,M); assertTrue(machine.get_cars().has(Car)); DELETE_CAR dc = new DELETE_CAR(machine); machine RoadFighter sees ctxt 0 variables objects lanes obstacles cars width height posX posY vel acc lean score collided active invariants objectsOBJECTS lanesLANES obstacles[cars = objects obstacles\cars = ? posX2objects!Z posY2objects!Z width2objects!N height2objects!N vel2cars!Z acc2cars!Z lean2cars!f-1, 0, 1g score2cars!Z collidedcars activeobstacles[cars events event initialisation then objects := ?lanes := ?obstacles := ?cars := ? posX := ?posY := ?width := ?height := ? vel := ?acc := ?lean := ?collided := ?active := ? end event update pos any car elapsed where car2cars elapsed2N then posX(car) := posX(car) + lean(car) elapsed1000 * 50 posY(car) := posY(car) + vel(car) elapsed1000 end Fig. 2. R OADFIGHTER : EVENT B model dc.run_DELETE_CAR(Car); assertFalse(machine.get_cars().has(Car)); } C. Experimental Results and Lessons Learned We developed a prototype of R OADFIGHTER in Android Studio SDK version 29 using Java with OpengGL 1.0. We used Eclipse Java 2020 to JUnit tests. We wrote the E VENT B model of the car racing in Rodin version 3.3. We used the last version available of the E VENT B2J AVA Rodin plugin to generate code for the E VENT B Model of R OADFIGHTER (the update site of E VENT B2J AVA is http://svrrodin.javerianacali. edu.co/EventB2Java UpdateSite Rodin3.2/). The Android Studio’s R OADFIGHTER implementation makes use of the Java code generated by E VENT B2J AVA. The Rodin project, the Eclipse project with the JUnit tests, and the implementation in Android Studio are available from https://github.com/ncatanoc/carracinggame. Table I summarizes R OADFIGHTER ’s development effort in EVENT B and Rodin. LOC stands for Lines of Code, and POs for the number of Proof Obligations generated by Rodin. The EVENT B model includes 1 abstract machine and 3 reﬁnement machines. Rodin’s provers discharged all the POs automati- cally. A Master student in Computer Science spent 2 weeks developing a previous and much simpler version of the model that contained only 1 machine. He spent some additional 2 weeks developing the Android Studio project that reuses the code generated by E VENT B2J AVA from the E VENT B model.Then, the ﬁrst authors spent additional 2 weeks extending the previous E VENT B model to include the 4 current machines. The Android Studio remained unchained (except porting ﬁle conﬁgurations to a more recent SDK version) as the ﬁrst author kept essentially the same events of the previous version. Lastly, the ﬁrst and second author spent 2 days writing the JUnit tests in Eclipse. The ﬁrst author discovered a small error in the deﬁnition of an event guard that he corrected in E VENT B and code-generated afterward. One of the most striking facts of our software development with E VENT B is that Rodin was able to discharge all the POs automatically. This is mainly due to the high performance of Rodin’s SMT prover (10 years ago it was a different story), but also at the way the E VENT B model is written, e.g., the model is deﬁned in terms of sets and relations and we put effort into not using quantiﬁed logical expressions. Machine LOC # POs % Aut. RoadFighter 82 22 100 ref0 circuit 187 67 100 ref1 kinectic 203 57 100 ref2 scoring 95 5 100 TABLE I ROADFIGHTER : STATISTICS FOR THE EVENT B M ODEL Our prototype implementation of R OADFIGHTER under- went a two-steps sanitization process. First, we discharged all the Proof Obligations in Rodin. Second, we manually wrote Java Unit tests for the code generated by E VENT B2J AVA. The ﬁrst process checks that the E VENT B model is sound, the second process veriﬁes that our understanding of the model is correct. Often times, when writing the unit tests for an event, we realized that the event guards are not correctly deﬁned in Rodin, making the test fail. Therefore, we corrected the event in Rodin, generated Java code again for the whole event, and re-run all the tests automatically in Eclipse. We summarize below some key aspects of this case study. (i:) Game apps (that are similar to R OADFIGHTER ) use ﬂoating-point values to model features such as object positions or dimensions. E VENT B implements integer arithmetic as opposed to ﬂoating-point arithmetic that one would need to implement the physical elements involved in a game. (ii:) Rodin’s provers managed to discharge all the POs of our E VENT B model automatically. Of course, the user’s expertise is required for proper modeling software applications in E VENT B. (iii:) Formal methods can be applied to non-critical systems such as R OADFIGHTER , unlike the popular disbelieve that advocates the use of formal methods for critical applications mostly. (iv:) Formal speciﬁcations help developers reason about re- quirements even before writing a single line of code. Analysis of requirements at the early stages of software development promotes the development of trustworthy software. (v:) The use of set theory in formal veriﬁcation helped us write mathematically sound speciﬁcations and model complex business logic in a very simple way. (vi:) E VENT B speciﬁcations provide great insight into how to write unit tests. A developer who has a basic under- standing of formal methods can easily port E VENT B speciﬁcations into unit tests. We think that a formal methods tool that generates unit tests from E VENT B models automatically must be implemented. IV. A C HAT APPLICATION The chat application is an application with functionalities similar to the WhatsApp app. It features functionality to send content, delete content, forward messages, etc. The chat appli- cation brings further challenges to the process of validation of functional software requirements with E VENT B, e.g., stronger interaction of events and complex machine invariants. The chat application shares some similarities with the car racing game app in Section III, e.g., both apps are Android apps. However, unlike for R OADFIGHTER , we do not develop an interface for the chat system here. The main goals of this case study are the following: (i.) To demonstrate how software requirements for a real-life application can unambiguously be speciﬁed. (ii.) To demonstrate how reﬁnement and code generation techniques can effectively be used in practice to validate software requirements early in software development. Early validation of software requirements seeks to re- duce the high cost of ﬁxing bugs in later software development phases [4], [3]. (iii.) To give software developers alternatives to the use of formal methods in application development in a way that is cost-effective. A. Functional Software Requirements Functional software requirements for the chat application are similar to those of WhatsApp (available from https:// www.whatsapp.com/android/). We elicited the requirements for the chat application from our own experience using (the SmartPhone version of) WhatsApp. The US-01 User Story below introduces a requirement that describes the functionality used for creating a chat session between “Me” and “You”. The chat may not yet exist (it is a fresh chat session). In addition to the User Stories, we wrote the 13 invariants. Section IV-B discusses how to encode some of these invariants in E VENT B. US-01 create-chat-session Description As a user, I want to create a chat session to communicate with You Acceptance Given : A chat session between Me and You does not exist Criterion When : I decide to create a chat session with You Then : A chat session between Me and You is created, but not between You and Me.B. The Event B Model Table II presents the machine structure of our chat ap- plication in E VENT B. The abstract machine ( MachineZero ) observes basic functionality for chat sessions. The ﬁrst ma- chine reﬁnement includes functionality to check whether chat content (text, video, picture) can be read or not. The second machine reﬁnement adds implementation details. For instance, it represents chat content as a sequence (rather than a set) of content items. Machine Observations MachineZero Basic functionality MachineOne Read and unread status MachineTwo Vertical reﬁnement TABLE II CHAT: EVENT BMACHINES STRUCTURE The event create-chat-session below encodes US-01 in EVENT B. It creates a chat session for user Meto chat with user Y ou. The symbol2is the set membership operator, user is the set of users who have signed up to the chat application. The symbol ^is the logical-and operator. Me7! Y ou is a pair of elements, and chat is a mathematical relation that keeps track of the chat sessions that have been created. Event guard @grd2 formalizes the Given condition of US-01. Action @act1 encodes the Then expression; it adds the pair Me7!Y ou to the set of existing chats. Guard @grd1 is a typing condition, it helps parsers and compilers infer the type ofMeandY ou. event create-chat-session any Me Y ou where @grd1 Me2user^Y ou2user @grd2 Me7!Y ou=2chat then @act1 chat := chat[fMe7!Y oug end We wrote in total 10 User Stories that relate to the ab- stract machine ( MachineZero ), for creating a chat session, selecting a chat, chatting, deleting content, deleting a chat session, muting a chat, unmuting a chat, broadcasting content, forwarding content, and unselecting a chat, respectively. Each User Story relates to the static part of the machine (variables, data structures, invariant, axioms), to its dynamic part (1 or more events), or both parts. Table III summarizes our E VENT B development effort in Rodin for the chat system. The two last columns tell the number and percentage of Proof Obligations that are automat- ically discharged by Rodin’s provers. As one might expect, the last reﬁnement has a lower success rate in discharging Proof Obligations automatically. This is partly because the last reﬁnement machine introduces several data reﬁnements. We present below the formalization of Invariant “it is never the case that chat content exists associated to a pair of users for which no chat session exists”. Expression chat[fug]returns Machine LOC # POs # Aut. % MachineZero 170 53 51 96 MachineOne 91 46 46 100 MachineTwo 114 39 33 85 TABLE III CHAT: STATISTICS FOR THE EVENT B M ODEL the set of users with whom user uis chatting. Hence, the chatcont E VENT B. @inv118u,c,su2user^c2content) (u7!c7!s2chatcontent)schat[fug]) Implementing Invarint “A chat session between two users may have a set of associated content available to either or both of them” requires a subtler analysis as it relates content, the sender, and the recipient of the content. We formalize this invariant as @inv6 below. @inv6 chatcontent2user7!(content7!P(user)) C. Software Design Decisions Events delete-content and remove-content are subtle events as their executions can easily break the machine invari- ants, whereis E VENT B’s overriding operator. Event delete- content below does not remove cfrom chat Y ou7!Me, e.g., @act2 content := content nfcg). If it does, it might break invariant @inv6 in Page 5: it might be the case that some user has sent that content to a group of users previously. If one removes that content, one would need to demonstrate that for any user uother than Methe range of chatcontent(u) is a partial function from contentnfcgtoP(user) , which is unprovable. This means that any direct implementation of a functionality deleting chat content either cannot remove the content from the lists of contents, or may delete it only if it does not exist in any other chat, which might be time- consuming to validate. event delete-content any Me Y ou c where @grd1 Me2user^Y ou2user @grd2 Me7!Y ou2active @grd3 Me2dom(chatcontent) @grd4 c2dom(chatcontent(Me)) @grd5 Y ou2chatcontent(Me)(c) then @act1 chatcontent(Me) := chatcontent(Me)  fc7!(chatcontent(Me)(c) nfY oug)g end D. Lessons Learned The Rodin project of the chat case study is reachable at https://github.com/ncatanoc/whatsapp. In the following, we summarize some key aspects of this case study. (i:) We advocate for the use of formal methods tools at the early stages of software development. The use of formaltools helped us validate the software requirements of the chat system and check for possible inconsistencies. (ii:) The case study presented here solely uses E VENT B (and not unit testing) to validate functional software requirements expressed as User Stories. There are a few advantages of using E VENT B for that purpose. (a)User Story acceptance criteria match the syntax of events in EVENT B. This enables the design and implementation of software tools for the (semi-) automatic translation of informal speciﬁcations to formal speciﬁcations. (b) EVENT B speciﬁcations can be reﬁned as desired. In other words, we can make our software design as abstract or concrete as we want. (iii:) Expressing informal software requirements as User Sto- ries helped us express them as events in E VENT B since their structure match. On the other hand, software in- variants are not typically written by software engineers as part of their software requirements documents, yet they are critical to E VENT B. (iv:) The correct behavior of a chat system depends on the correct functioning of multiple people chatting concur- rently. Our work does not account for the performance of several chats running in parallel. Performance would require an architectural analysis. V. R ELATED WORK E. Stachtiari et al. [14] introduce an approach for the spec- iﬁcation of system requirements, and the derivation of system properties, which should be implied by the system struc- ture. System design is carried out with the BIP (Behaviour- Interaction-Properties) framework. Their approach is to be applied during the early stages of software development. They can build an executable model of a system starting with their system requirements. BIP and the E VENT B language that we use in our work are both models of transition systems. One advantage of using E VENT B is that it enables the deﬁnition of software reﬁnements from the most abstract machine all the way down to code. The use of textual boilerplates to express software require- ments is not a new idea. M. ´Smiałek et al. [13] propose a notation to express software requirements suitable for their translation into design models and code. Requirements are written in an SVO (Subject-Verb-Object) format and then transformed into a sequence of User Stories. SVO notation could be incorporated in our work to initially express software requirements, which then are translated to our User Story textual templates, and then to E VENT B. S.-P. Miller et al. [9] describe a case study conducted to determine if formal methods can be used in practice to validate requirements early in the software development process at some reasonable cost. The formal methods RSML and NuSMV are used to model the software requirements and the PVS system to conduct the underlying proofs. They claim their case study demonstrates that formal methods and formal models can effectively be used in realistic systems (an avionic system with several hundred requirements) to ﬁnd errors before implementation starts. Their case study is for a ﬂight guidance system. Our work is not necessarily related to safety-critical systems. VI. C ONCLUSION Our work focuses on the use of Formal Methods for model validation (as opposed to using Formal Methods for program veriﬁcation). We manually translate User Stories to formal speciﬁcations in E VENT B. Our ﬁrst validation check is carried out with Rodin’s type-checker, which checks for each E VENT B model that all its variables, constants, events, and the rest of its constructs are well-typed. Rodin raises an error in case it cannot infer the type of any construct. The second validation check is achieved through the generation of Proof Obligations that attest to the correctness of the E VENT B model. Rodin generates several types of Proof Obligations [7]. It generates a feasibility Proof Obligation for each action of every event stating that a solution (a program) for the assignment exists. It also generates Proof Obligations that relates a blueprint and its reﬁnement. For instance, simulation Proof Obligations ensure that abstract event actions are cor- rectly simulated by concrete actions. Rodin provers are semi- automatic in that they only assist users in discharging the Proof Obligations. The last validation check relies on the soundness of the code generator. The translation from E VENT B to Java (or any other implementation language) must be sound in order for the Java program to attest to the E VENT B formal speciﬁcation. A formal soundness proof for the code generation performed by EVENT B2J AVA has already been conducted [5]. [10] Nur Nurmuliani, Didar Zowghi, and Sue Fowell. Analysis of Re- quirements V olatility during Software Development Life Cycle. In 15th Australian Software Engineering Conference (ASWEC 2004), 13-16 April 2004, Melbourne, Australia , pages 28–39. IEEE Computer Society, 2004.