SOFTENG 752 Formal Specification and Design Assignment #1: Formal Modelling
SOFTENG 752
Formal Specification and Design
Assignment #1
Due: 5pm, Friday 25 August 2023.
Problem description
The formal specification techniques that are introduced in this course represent powerful methods for expressing complex concepts and have wide applicability across numerous research fields. They encompass a range of theories, methods, and languages, and by applying these techniques, you can significantly enhance the quality of software design.
These enhancements come in the form of a more precise description of the system, allowing for rigorous verification of its functionality. This helps in ensuring that the software system under development meets the intended specifications and behaves in an expected manner. The precision and rigour afforded by these techniques can reduce errors and ambiguities, leading to a more reliable and robust product.
In this particular assignment, which constitutes 15% of your overall grade, you are tasked with leveraging these principles. You will be required to use the B formal modelling language to specify the design of a software system in an exact and unambiguous way. You must also use the associated tool, i.e., the ProB model checker, to validate and analyse the design, checking for consistency, completeness, and correctness. It helps in providing evidence that the design accurately represents the intended behaviour of the system, and it helps in uncovering any hidden errors or inconsistencies.
Your options for this assignment are flexible. You can either choose one of the suggested systems provided below, each with its own unique challenges and requirements, or find a system of your own choosing. This allows you to tailor the assignment to your interests and expertise, making it a more engaging and meaningful experience.
Once you’ve selected the system, you will then need to embark on a com- prehensive process. First, collect all the relevant requirements, carefully under- standing what the system is supposed to achieve. Then, analyse and document the design in a detailed manner, outlining the structure, behaviour, and interactions within the system. Finally, validate the design using the aforementioned tools and techniques, ensuring that it meets all the specified requirements.
This assignment not only assesses your grasp of the formal specification techniques but also fosters a deep understanding of the software design process. It offers a hands-on experience with state-of-the-art tools and practices, preparing you for the challenges and opportunities in the ever-evolving field of software engineering.
• Online Shopping System
• Library Management System
• Email Client/Server System
• Multi-Lifts Control System
• Smart Home Security System
• Petrol Station Management System
• Police or Ambulance Dispatch System
• Travel Booking Management System
• Part 4 Project Management System
• Online Chatting System
• Air Traffic Control System
• Public Transportation Management System
• Online Banking System
• Train Control System
• Hotel Reservation System
• Warehouse Management System
• Event Management System
• Virtual Learning Environment (VLE) System
• E-Voting System
• Fitness and Health Tracking System
• Automated Parking System
• Inventory Control System
For this assignment, you are required to choose a real-world system and create a design model based on its actual applications and scenarios. This means you will need to thoroughly investigate and understand the functional requirements of your selected system as they apply in real-world contexts. Your task is to translate these functional requirements into a formal specification and validate it using the tools and techniques you’ve learned in the course. The specific tasks required for this assignment are listed as follows:
-
Document the Functional Requirements: In a detailed report form, de- scribe the functional requirements of the system under design. This in- cludes identifying the key functions, behaviours, and interactions that the system must exhibit in its real-world application.
-
Create a B Formal Specification and Verify the Design: Utilise the B for- mal modelling languages to construct a precise specification of the system under design. You’ll then need to simulate and verify the design model us- ing the ProB model checker, an essential tool for ensuring the consistency and accuracy of your design.
-
Document the B Design Model and Verification: Prepare a comprehensive report that documents both the B design model and the verification process. This should include a detailed explanation of the model, the methods used for verification, and the outcomes of the verification process.
You have the option to approach this assignment as a single person task or collaborate with a partner, in a group of no more than two students. Whether working alone or with a partner, the focus should be on applying formal specifi- cation techniques to a real-world scenario, demonstrating a deep understanding of the principles taught in this course.
By engaging with the tasks described above, you will not only gain practical experience in applying formal specification techniques but also cultivate valuable skills in translating real-world problems into formal, analysable models. This assignment serves as an opportunity to synthesise the concepts learned in the course and apply them to a tangible, real-life system, paving the way for your future work in the field of software design and analysis.
Files to submit
-
Submit a B Formal Specification Model: Provide your B formal specifica- tion model in the ProB supported syntax format. This ensures that it can be readily loaded and simulated using the ProB tool, enabling verification and analysis of your design.
-
Submit a Report in PDF Format: Your report should be submitted in PDF format and must not exceed 5 pages, with single-spaced 11/12pt text. The report should focus on describing the system requirements, explaining the B model, and discussing the properties that can be verified, among other relevant details.
-
Group Work Instructions (if applicable): If you choose to work in a group of two students on this assignment, you may submit the same B specifica- tion model. However, the report must be individually written, reflecting your unique insights and understanding. Please include the name of your assignment partner in your submission if working in a group.
Assessment
The assignment will be assessed for 100 marks in total, which equates to 15% of the final grade. The grading consists of:
-
B Specification and System Property Modelling (70 marks): The mod- elling portion will be assessed on various criteria, including:
-
– Conciseness and Correctness (20 marks): Evaluate the effectiveness and accuracy of the model.
-
– Complexity and Completeness (20 marks): Assess the depth and completeness of the specification.
-
– Structure and Properties (20 marks): Analyse the organisation and defined attributes of the model.
-
– Validation of Design (10 marks): Check the validation methods ap- plied to the design.
-
-
Written Report of the Formal Modelling and Discussion (30 marks): The written report will be assessed for:
-
– Clarity of the Explanation (10 marks): Assess how well the require- ments, B model, and verifiable properties are explained.
-
– Discussion and Presentation (10 marks): Evaluate the quality of dis- cussion and the presentation of the findings.
-
– Aspects Referring to Verification (10 marks): Analyse the content that refers to the verification of the model, including methods and results.
These criteria provide a comprehensive and detailed assessment of both the technical modelling and the written explanation, ensuring a well-rounded eval- uation of the student’s understanding and ability.
The due date of assignment 1 is Friday 25 August 2023, 5:00PM.
