Formal Methods

 

Current information in 2021 (spring semester)

• From 2021, new information and course materials will be posted to the Faculty's Moodle system.
• Below you can find archived information from 2020.

 

Archive contents (2020)

• News
• Objectives and synopsis
• Materials
• Assessment and recaps
• Midterm exams
• Homework assignment
• Topics for the final exam

Announcement about distant teaching from the 23rd of March, 2020

• 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).
• 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/Guide-lines%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/formal-methods/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: Kripke-structures, 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 state-dependent 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 Petri-net formalism. Dynamic properties of Petri-net 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 Petri-nets. Modelling examples.
• Modelling data-dependent behaviour: The extension of Petri-nets 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 extra-functional properties: The extension of Petri-nets with probabilities and time: Stochastic Petri-nets. 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, counter-example 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 small-scale 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)
• Repetition (retake) of the first midterm exam (RME1)
• The second midterm exam (ME2)
• Repetition (retake) of the second midterm exam (RME2)
• Additional retake (RRME)

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:
  • ME1A solution 
  • ME1B solution
• Scores and grades: [0-15) fail, [15-20) pass, [20-25) satisfactory, [25-30) good, [30-35] 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.
  • 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.1-5.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 2020-03-23)

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 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 solution:
  • RME1 solution
• Scores and grades: [0-15) fail, [15-20) pass, [20-25) satisfactory, [25-30) good, [30-35] excellent.
• Results:
  • Login to the Homework portal and you will find the results under “RME1 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:
  • The principles are basically the same as in case of ME1.

Detailed information about writing RME1 (updated on 2020-04-04)

The midterm exam is organized using online (internet based) techniques in the same way as in case of the first midterm exam (please check the related details and advice above).

• At 18:00 please login to the homework portal (https://hf.mit.bme.hu). Here, regarding the Formal Methods subject, you will find an "RME1 (English)" row. Please click on this row and you can find in the "URL" field the URL of the exercises (the link will appear at 18:00).
• 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 your full solution does not exceed 10 MB. 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 to the homework portal until 19:20 (uploading is allowed from the start of RME1, thus if you are ready earlier then you can upload your file). Uploading is possible on the same page where the URL of the exercises was provided.

The second midterm exam (ME2)

• Date: 19 May, 2020 (Tuesday), 18:00. The midterm exam is organized using online (internet based) techniques. Detailed information is available below.
• Topics:
  • The lectures that were not included in ME1: Lectures 06, 08-12 on the Materials page of the course.
  • Note that Stochastic Petri nets is not part of ME2.
• Reference solutions:
  • ME2A solution 
  • ME2B solution
• Scores and grades: [0-15) fail, [15-20) pass, [20-25) satisfactory, [25-30) good, [30-35] excellent.
• Results:
  • Login to the Homework portal and you will find the results under “ME2 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 concrete problem to the course coordinator (majzik@mit.bme.hu).
• Basic principles of the evaluation (please note that it is not possible to list all of the potential problems here; problems or mistakes not mentioned here may also result in reducing the score):
  • 1.a) Missing CFA state, state transition, or label results in -1 point.
    1.b) Only a complete and correct answer results in 1 point.
    1.c) 0 point in case of incorrect answer or missing explanation, max. 1 point if the explanation is incomplete or contain mistakes.
  • 2: 1 point for understanding each of the following concepts: weights, inhibitor arcs, places with finite capacity, covered places, w label, loop edges in the coverability graph; -1 point for mistakes (e.g., incomplete coverability graph, wrong labels etc.).
  • 3: Full score if the correct matrix operation is described; -1 point if there is a problem with the understanding of the invariants or matrix operations.
    In 3.d), the statement that the condition does not hold in the initial state results in 0.5 point; the checking of the P-invariant results in 0.5 point, the correct explanation results in 1 point.
  • 4: Each correct property results in 1 point.
  • 5: Incomplete answers result in reduced score.

Detailed information about writing ME2 (updated on 2020-05-14)

The midterm exam is organized using online (internet based) techniques in the same way as in case of the first midterm exam (please check the related details and advice above).

• 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 it was in case of uploading 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 "ME2 group" row. According to the value found here (ME2A or ME2B) please click on the corresponding ME2A or ME2B 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 is 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 "ME2 group" row. According to the value found here (ME2A or ME2B), please click on the corresponding ME2A or ME2B 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 is provided. 
    The submission deadline is 19:35.
• 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 your full solution does not exceed 10 MB. 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 to the homework portal until the deadline given above (uploading is allowed from the start of ME2, thus if you are ready earlier then you can upload your file). Uploading is possible on the same page where the URL of the exercises was provided.

Repetition (retake) of the second midterm exam (RME2)

• Date: 28 May, 2020 (Thursday), 10:00. The midterm exam is organized using online (internet based) techniques, in the same way as in case of the first midterm exam (please check the related details and advice above).
  Detailed information is available below.
• Topics:
  • The lectures that were included in ME2: Lectures 06, 08-12 on the Materials page of the course. Note that Stochastic Petri nets is not part of RME2.
• Reference solution:
  • RME2 solution
• Scores and grades: [0-15) fail, [15-20) pass, [20-25) satisfactory, [25-30) good, [30-35] excellent.
• Results:
  • Login to the Homework portal and you will find the results under “RME2 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 concrete problem to the course coordinator (majzik@mit.bme.hu).
• Basic principles of the evaluation:
  • The principles are basically the same as in case of ME2.

Detailed information about writing RME2 (updated on 2020-05-24)

The midterm exam is organized using online (internet based) techniques in the same way as in case of the first midterm exam (please check the related details and advice above).

• At 10:00 please login to the homework portal (https://hf.mit.bme.hu). Here, regarding the Formal Methods subject, you will find an "RME2 (English)" row. Please click on this row and you can find in the "URL" field the URL of the exercises (the link will appear at 10:00).
• 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 your full solution does not exceed 10 MB. 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 to the homework portal until 11:20 (uploading is allowed from the start of RME2, thus if you are ready earlier then you can upload your file). Uploading is possible on the same page where the URL of the exercises was provided.

Additional retake (RRME)

• Date: 9 June, 2020 (Tuesday), 16:00. The midterm exam is organized using online (internet based) techniques. 
  Detailed information is available below.
• Topics: The topics of the midterm exam that is to be retaken.
  • Any of the two midterm exams (ME1 or ME2) can be retaken, but only one of them.
  • This opportunity can also be utlized to improve your grade. However, please note that according to the BME Code of Studies (Title 28), in case of repeated evaluation of learning outcomes, the result of the repeated evaluation (in this case the result of RRME) will be considered, even if it is worse than the original grade.
  • Study material is available on the Materials page of the course.
• Reference solution: TBA
• Scores and grades: The same as in case of ME1 or ME2.
• Results:
  • Login to the Homework portal and you will find the results under “RRME score”.
  • The scores can be checked by comparing your solution with the reference solution.
  • If you find a mistake in the evaluation of your solution then send an email with the detailed description of your concrete problem to the course coordinator (majzik@mit.bme.hu).

Detailed information about writing RRME (updated on 2020-06-04)

The midterm exam is organized using online (internet based) techniques in the same way as in case of the first midterm exam (please check the related details and advice above).

• At 16:00 please login to the homework portal (https://hf.mit.bme.hu) and select the Formal Methods subject.
  • If you would like to retake ME1 then please click on the "RRME1 (English)" row and you can find in the "URL" field the URL of the exercises (the link will appear at 16:00).
  • If you would like to retake ME2 then please click on the "RRME2 (English)" row and you can find in the "URL" field the URL of the exercises (the link will appear at 16:00).
• 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 your full solution does not exceed 10 MB. 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 to the homework portal until 17:20 (uploading is allowed from the start of RRME, thus if you are ready earlier then you can upload your file). Uploading is possible on the same page where the URL of the exercises was provided.

---

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: 10th day of the examination period