University Management System: a B method project
Introduction
It is a true challenger to guarantee that the software is correct and safe while the software executes. However, some systems need extremely guarantee those two conditions to be used by the consumer. Those systems are, mostly, critical systems. Critical systems are a system that a minimal error of the system can generate huge negatives impacts. As examples of those systems are a system of a nuclear plant or an automatic pilot of an airplane.
To the developer of those systems is need to guarantee that each system will work correctly and there is any fault in the code and the execution. In software engineering, there are many ways to indicate even to guarantee that the software is correct and safe. One of those ways is the use of formal methods. Formal methods use a strong base mathematical to be able to inform that the software satisfies some properties like deadlock, livelock, etc. The verification of those properties helps to indicates that the system is correct and safe to use.
On companies, the software development that needs to use formal methods in your verifications came attached to the use of tools like FDR4 or Atelier B. Those tools have the proof of the verification automated getting information on the specification of the system. These specifications are written use of languages like the B method, CSP, or Z.
This article has the goal to show the principles and properties that are used on a project that uses formal methods. To show those will be described in this article one simple project developed in the B method and using the Atelier B as an auxiliary tool.
The B method
The B Method is a formal, model-oriented language that uses the concept of an abstract machine to develop specifications that allow the incremental through the concept of refinement. A machine, in the B method, is an encapsulation that holds information about itself, information as of the state of the machine, defined by a set of variables, and the set of operations that the machine can operate.
There are three classifications to a machine in the B Method, these are abstract machines, refinement machine, and implementation machine.Abstract machines are used to describe the specification using non-deterministic and first-order logic in your development. Refinement machines are used to remove the non-deterministic used in the abstract machine and substitutes with deterministic and analogous operations in the specification. At least, the implementation machines are those where there is no non-deterministic in your specification, even allowed the conversion to another language like C. Using the tool Atelier B is possible to make this conversion in an automatic way to the user.
The abstract machines in the B method are divided into two aspects, static and dynamic. On the static aspect of the machine can define the sets, constants, properties, variables, and invariant of the machine.
The SETS, define the name of a set, CONSTANTS create variables that can not change, PROPERTIES define the constants with a predicate, VARIABLES creates variables. The INVARIANT defines the variables of the machine as a predicate, this predicate can use the sets created to define the variables and works like pre-requirement to the machine.
On the dynamic aspect, is where the variables are initialized by substitution and defined the operations of the machine. The operation structure has a pre-requirement to the machine be able to use. If this pre-requirement be satisfied the operation would be used and this operation can return or not an answer.
The machines also can see or include other machines. If machine A sees machine B, machine A can use, case the pre-requirement is satisfied, the operation of machine B that returns an answer. If machine A includes machine B, machine A has access to variables, sets, and operations defined on machine B.
The Project
The project that this article will talk about is a simple system to manage a university as all. To be able to run a university the system, use the strategy of divide and conquer, where the university is divided into some smaller parts and forward in machines in the code. Some machines in the system are only to represents a set that is used in other machines in the system. These sets represent the set of students, professors, classes, careers, and departments. Theses machines are named with the suffix ‘ctx’. The other machines are named with the suffix ‘Mch’, an example is the machine StudentMch, which will be explained after in this section.
Starts from the top to down, the machine that represents the department can see the sets of careers, professors, and departments. The machine also has variables to represents the coordination, the members, and the career. Those are defined into the invariant. The coordination is defined as a partial function, how the domain is the set of professors and the image is the set of careers. The members are a partial function from the set of professors to the set of departments and the career is a partial function from the set of careers to the set of departments. Also in the invariant was defined as the cardinality of coordination, 2 <= coordination >= 0. The variables are initialized as an empty set. The machine has operations to add and remove professor member of the department, add and remove career to the department, and coordination.
The machine that represents the career, can see the machines subject and department and the sets of students, careers. The variables of this machine represent the required and optional subjects and the enrolled students, defined in the invariant. The variable that represents the required and the optional subjects is defined as a relation between the sets of careers and subjects. The enrolled students are defined as a partial function from the set of students to the set of careers. Those variables are initialized as an empty set. The machine can add and remove the relations of students to careers, required, and optional subjects.
The machine that represents the class, can see the subject, professor, career and department machines, and the set of students. Unlike the machines described above, this machine includes machine studentMch. The variables describe the classes, the sum score of a student, and your quantity of exams. The class is defined as a relation between professor and subject. The sum score is a total function from student to a range started on 0 to 30 and the number of exams is also a total function from student to the range 0 to 3. The variable that represents the classes is initialized as an empty set. The sum score and the number of exams started at 0. The machine can create and remove a class, add and remove a student, add a score of an exam of a student, this operation will return the new average score of this student. Also is possible to get directly the average score and the number of exams that the student has. The machine also sees if the student has the average to pass the subject.
To represents the subject the machine has only the variable to represent the set of previous subjects required to be able to do other subjects. This variable is defined as a relation of the set of subject to subject, initialized as an empty set. The machine can add and remove a subject as a previous requirement to a subject.
The machine to the student can see the set of students and the subject and career machines. Has a variable to represent the approved subjects defined as a relation of students and subject, that is initialized as an empty set. The machine can only add an approved subject to the variable.
Conclusion
This article was shown a simple system of a university manager that was developed to use the B method. To verify the correctness of the system was used Atelier B to make and prove automatically the proof obligations. The tool has proved 97% of all verifications of the system. It is also able to convert this code written with the B method to the programing language C. The development of the implementation machines of the system is defined as the future work of this article. The code of this project is available here
