This repository contains a collection of exercises and projects related to formal methods in computer science. Developed during the Formal Methods for Computer Science course at the Department of Computer Science, University of Bari "Aldo Moro", under the supervision of dr. Berardina Nadja De Carolis, these materials explore various formal methods and their applications.
The repository is organized into several exercises, each focusing on different formal methods:
-
Exercise 1: Finite State Machines (FSM) for Non-Player Characters (NPC)
- Design and implementation of FSMs to model NPC behaviors in gaming applications.
-
Exercise 2: Finite State Machines (FSM) for Non-Player Characters (NPC) with LLMs
- Integration and simulation of the modeled NPC behaviors using Large Language Model as agent.
-
Exercise 3: ITEMIS ATM
- Modeling and analysis of an Automated Teller Machine (ATM) system using ITEMIS, focusing on statecharts and system transitions.
-
Exercise 4: NuSMV Elevator
- Verification of an elevator control system using the NuSMV model checker, emphasizing temporal logic specifications (LTL properties).
-
Exercise 5: Process Mining - Loan Application
- Application of process mining techniques to analyze and optimize a loan application process, employing PM4Py and LLMs to improve the quality of the discovered process model.
This project delves into finite state machines, formal methods, Petri nets, model checking, process mining, statecharts, and related topics, providing practical implementations and analyses pertinent to computer science.
finite-state-machineformal-methodspetri-netsmodel-checkerprocess-miningstate-chartspm4pyitemisnusmv-model-checkerllm
This project is released under the LICENSE. See the LICENSE file for details.