Formal Methods
Contents
Announcement about distant teaching from the 23rd of March
 The lectures of the course will be delivered using online techniques, according to the schedule of the original timetable: each Monday, 12:15  15:00.

You may join directly in the MS Teams application (registration details see below) or using the link provided here.
 30 March. 2020 (Monday) 12:1515:00 online lecture

23 March, 2020 (Monday), 12:1515:00 online lecture
 The MS Teams application will be used for lectures and homework consultations. Please create an account (eduID address) as soon as possible, based on the explanation given in the Guidelines for distant education (https://www.vik.bme.hu/document/3169/original/Guidelines%20for%20distan...).
 After setting up your Teams account, you will find the lecture invitations in the "Formal Methods  VIMIMA07EN" team. (The required link will also be provided here just before the starting time of the lecture.) If you do not find this team then please inform the course coordinator (majzik@mit.bme.hu).
 The lecture will consist of the presentation of slides (sharing slides and sound). No extra preparation is required (besides accessing the Teams system). There will be no record of attendance on lectures.
 The slides presented during the lecture will be made available for offline studying, as usual at the Materials page of the course (https://inf.mit.bme.hu/en/edu/courses/formalmethods/materials).
Objectives
As the complexity of information systems and the costs of potential failures are increasing, it becomes more and more important to prove that the design of the critical system components is correct. One of the typical solutions for the challenge of provably correct design is the application of formal methods. Formal models allow the precise and unambiguous specification of requirements and construction of designs; formal verification allows the checking of design decisions and proof of design properties; while the verified models allow automated software synthesis. The subject provides an overview of the formal background needed for the elaboration and analysis of the formal models of IT components and systems: the modelling paradigms, the widely used formal modelling languages, and the related verification and validation techniques. The subject demonstrates the application of formal methods in the field of requirement specification, system and software design, model based verification and source code synthesis.
The participants of the course who pass the requirements will be able to
 understand and apply various formal methods;
 construct formal models on the basis of informal descriptions;
 understand the advantages and disadvantages of various formal verification techniques;
 and apply tools that support the application of formal methods.
Synopsis
 Formal modelling and analysis of information systems (introduction to the subject): The role of formal methods during the design and development of IT systems: formal requirement specification, modelling, verification (model checking and proof of correctness). The relation of engineering and formal models, model transformations. Design environments that support the application of formal methods (e.g., SCADE).
 Basic formal models and their semantics: Kripkestructures, transition systems, timed automata, network of timed automata.
 Formalization of requirements: Temporal logics: linear time temporal logic (LTL), branching time temporal logics (CTL, CTL*). The comparison of their expressiveness. Practical examples and applications: the Property Specification Language.
 Formal verification using model checking: Model checking by the tableau method. Symbolic model checking. The representation of the state space using reduced ordered binary decision diagrams. Bounded model checking. Verification of time dependent behaviour. Practical applications: Modelling embedded controllers using timed automata, verification of temporal properties, automated test case generation using model checkers. The UPPAAL model checker.
 Modelling statedependent dynamic behaviour: The formal syntax and semantics of statecharts. Design using statecharts, the formal verification of properties. The typical patterns for software synthesis. Practical applications: UML 2 statecharts, software source code generation and monitor synthesis.
 Modelling and analysis of concurrent systems: The Petrinet formalism. Dynamic properties of Petrinet models (e.g., safety, liveness, boundedness). The verification of dynamic properties by simulation or on the basis of the reachability graph. Structural properties (e.g., conservativeness, consistency, invariants) and their analysis on the basis of the state equation. Property preserving model reduction techniques. Hierarchical Petrinets. Modelling examples.
 Modelling datadependent behaviour: The extension of Petrinets with data types and data processing. The adaptation of the definitions of dynamic and structural properties. Practical applications: Analysis of the consistency of distributed data processing, protocol verification.
 Specification and verification of extrafunctional properties: The extension of Petrinets with probabilities and time: Stochastic Petrinets. Formalization of properties using stochastic temporal logic. Verification of performance and dependability properties.
 Modelling data processing: The syntax and semantics of data flow networks. Model refinement, checking the consistency of model refinement. The application of data flow networks for modelling and analysis of business processes.
 Formal verification based on software source code: Model checking C programs. The use of abstraction: static analysis using abstract interpretation, predicate abstraction, counterexample guided abstraction refinement in model checking.
Materials
Slides, models, and other documents can be found on the Materials page.
Assessment and recaps

During the semester: The requirements for passing the subject are 2 successful midterm exams and a successful homework.
 The homework includes modelling of a smallscale IT system and the verification of its required properties. The homework is assigned on the 4th week of the semester and it has to be submitted and presented from the 10th week of the semester.
 The final grade of the subject is calculated from the grades of the two midterm exams (taken into account with weights 35%35%) and the grade of the homework (taken into account with weight 30%).

Recaps:
 Each midterm exam can be repeated once, and there is an additional retake possibility.
 The homework can be submitted during the repetition period, but this late submission will result in 20% decrease of the score. The submission of the homework cannot be replaced by a repeated midterm exam.
 In the examination period: 
Midterm exams
The first midterm exam (ME1)

Date:
17 March, 2020 (Tuesday), 18:15.According to the university level measures, the new date of the first midterm exam is 24 March, 2020 (Tuesday), 18:00. The midterm exam is organized using online (internet based) techniques. Detailed information is available below. 
Topics:
 The first 5 lectures. Slides and examples are on the Materials page.
 Reference solutions:
 Scores and grades: [015) fail, [1520) pass, [2025) satisfactory, [2530) good, [3035] excellent.

Results:
 Login to the Homework portal and you will find the results under “ME1 score”.
 The scores can be checked by comparing your solution with the reference solution above.
 If you find a mistake in the evaluation of your solution then send an email with the detailed description of your problem to the course coordinator (majzik@mit.bme.hu).

Basic principles of the evaluation (please note that it is not possible to list each potential problem here; problems or mistakes not mentioned here may also result in reducing the score):
 1.1. Correct answer is 1 point, incorrect answer is 0 point.
 1.2. 1 point for each expression that does not hold although it shall hold, or does hold although it shall not hold. 1 point for each additional state in the state sequence that is not necessary (but max. 2 points).
 1.3. 0 point, if the temporal logic expression is not a correct solution of the task. LTL expression without path quantifier is 0 point.
 2. Reduction of the score: 1 point if there are too many states. 0.5 points if a label of a system level state is not correct. 1 point if there are missing transitions, or extra transitions. If there are more than one mistakes regarding the states or transitions then additionally 1 point. 0 or 1 point if the solution has essential problems.
 3.1. 0.5 point if the characteristic function of the initial state is correct. 1.5 points if the characteristic function of the path is correct. Each error may result in 0.5 point.
 3.2. 0 point if the diagram is not correct and there are no details (steps) how the diagram was constructed. 1 point for the formula of the function or the binary decision tree of the function. 2 points if the diagram is almost correct but there are missing merging or reduction steps. Accidental errors may result in 0.5 point.
 4. In case of ME1A: “not p” labeling for states S, A: 1 point. “EX q” labeling for states B, C: 2 points. “A((not p) U (EX q))” labeling for states B, C: 1 point. “A((not p) U (EX q))” labeling for state S: 1 point. “A((not p) U (EX q))” labeling steps are precisely described: 1 point. If it turns out that the labeling algorithm is not correct (or steps are missing) then it may result in further reduction of the score.
 4. In case of ME1B: “AX p” labeling for states S, A, C, D: 2 points. “E((AX p) U q)” labeling for states A, D, then for state C in separate iteration: 1 point. “q” label is taken into account correctly in the iteration: 1 point. “E((AX p) U q)” labeling for state S: 1 point. “E((AX p) U q)” labeling steps are precisely described: 1 point. If it turns out that the labeling algorithm is not correct (or steps are missing) then it may result in further reduction of the score.
 5.15.3: 0.5 point if the temporal logic operator is almost correct (but the syntax is not, or operands are missing). 1 point if the operator and its syntax is correct. 1.5 points if there are only minor mistakes. 2 points if the complete expression is correct. 0.5 points if the G operator is missing.
 5.4: 1 point for the negation of the expression before constructing the tableau. 1 point for handling the U operator in the tableau. 1 point if the construction of the tableau was correctly started. 2 points for a complete tableau with edges to existing nodes. 1 point for giving the counterexample explicitly (marking on the tableau is not sufficient).
Detailed information about writing ME1 (updated on 20200323)
To solve and submit ME1, you need the following:
 Internet connection.
 Web browser and PDF reader to access and read the exercises.
 Dark pen (blue or black) and empty sheets of A4 paper (at least 3 sheets) to prepare your solution.

Digital camera, document scanner, or mobile phone with camera or scanner application (e.g., Cam Scanner, Office Lens, Genius Scan) to digitize your solution in PDF or JPG format.
If it is not possible for you to digitize your solution, then this midterm exam cannot be passed. Considering such technical issues, there is an additional retake possibility at the end of the semester (using different online techniques).
The exercises will be available and the solutions shall be submitted electronically (details are provided below) in the following steps:
 At the starting time of ME1 you have to login to the portal, find and read/download the exercises.
 Solve the exercises by handwriting and drawing of diagrams on your sheets of paper. Please start solving each exercise on a separate page. On each page, please write your name, Neptun code, and signature.
 60 minutes are available for solving the exercises.
 Then digitize the pages containing your solution into PDF (preferred) or JPG format, with a resolution that is well readable, but ensures that the size of a digitized page does not exceed 1 MB (approx.. 300 dpi; if needed, you may resize your images, increase contrast, etc. using image processing tools). If you digitize into PDF then merge all pages into a single PDF document. If you digitize into JPG then add your files to a single ZIP package.
 Upload your PDF document or ZIP package (uploading is allowed from the start of ME1, thus if you are ready earlier then you can upload your file). The maximum size of the file that can be uploaded is 10 MB.
 20 minutes are available to digitize and upload your files (after the time period available for the solution of the exercises). After 60+20 minutes following the start of ME1, submission will not be accepted.
Access to the exercises and submssion of the solution:
Access to the exercises and submission of the solution will be possible on the https://hf.mit.bme.hu portal of the department. You can login with the BME Central Login system (in a similar way as in case of accessing your homework assignment). In order to reduce the load of the portal, there will be slightly different starting times and submission deadlines:
 If your homework assignment is HA01 then please login to the portal at 18:00. Here, regarding the Formal Methods subject, you will find an "ME group" row. According to the value found here (ME1A or ME1B) please click on the corresponding ME1A or ME1B row below. Here the "Link" field will provide you the URL of the exercises (the link will appear at 18:00). The submission of the digitized solution (PDF or ZIP file) will be possible on the same page where the URL of the exercises was provided. The submission deadline is 19:20.
 If your homework assignment is HA02 then please login to the portal at 18:15. Here, regarding the Formal Methods subject, you will find an "ME group" row. According to the value found here (ME1A or ME1B), please click on the corresponding ME1A or ME1B row below. Here the "Link" field will provide you the URL of the exercises (the link will appear at 18:15). The submission of the digitized solution (PDF or ZIP file) will be possible on the same page where the URL of the exercises was provided. The submission deadline is 19:35.
Advice:
 Practice in digitizing your A4 sheets. It is not good if you start learning and trying the necessary application during the exam. Considering the digitized images of your pages, these must be readable: we can evaluate only the pages that can be easily read (in case of blurred images, wrong focus, etc. we will not guess what your solution is).
 The separation of the periods (60 minutes for the solution and 20 minutes for digitizing and uploading your pages) is recommended to ensure that your pages are digitized and uploaded in time. Please upload your documents as soon as possible, since in the last minute the server may slow down due to overload.
 During ME1, several problems may occur considering the access to the server, digitizing and uploading your documents (broken internet connection, the overload of the network, crash of your applications, etc.). We cannot handle and take into account these problems: we will evaluate only the solutions that were uploaded to the server. Please do not send error reports or your solution in email or other ways. Considering the possibility of such problems, there are two retake options (normal retake of ME1 and also an additional option at the end of the semester).
 Please keep your solution both in physical and in electronic format.
Good luck and we hope that there will be no technical problem during ME1!
Repetition (retake) of the first midterm exam (RME1)

Date:
31 March, 2020 (Tuesday), 18:15.7 April, 2020 (Tuesday), 18:00.  The midterm exam will be organized using online (internet based) techniques. Further information will be provided later.

Topics:
 The first 5 lectures. Slides and examples are on the Materials page.
 Results: See later
The second midterm exam (ME2)
 Date: 19 May, 2020 (Tuesday), 18:15.
Repetition (retake) of the second midterm exam (RME2)
 Date: 28 May, 2020 (Thursday), 10:15.
Additional retake (RRME)
 According to the university level measures, a further freeofcharge opportunity will be provided for the retake of the midterm exams (any of the midterm exams, but only one of them, even for purpose of improvement of grade), by the tenth day of the examination period. Further details will be provided later.
Homework assignment
 Details of the homework are on the Homework assignment page.
 Submission deadline for the homework: 9 May, 2020 (Saturday), 23:59:00
 Late submssion of the homework: 27 May, 2020 (Wednesday), 23:59:00