Formal modelling of a Facebook-like social network in VDM++ using the Overture Tool, developed for a Software Engineering Formal Methods class (MFES) @ MIEIC, FEUP. Done with antonioalmeida and diogotorres97.
| Folder | Foder Content |
|---|---|
| VDM++ | Facebook modelation in VDM++ |
| Java | Automatically generated code from VDM++ as well as an additional User Interface to make interaction with the Facebook model easier |
Development is thoroughly specified in our report. Our Facebook-like social network includes users, their respective timelines (i.e., posts made by them) with different access permissions, group chats and consisting messages.
In the report, we start by identifying a formal list of requirements, as well as both Use Case and Class UML diagrams. The former can be found below.
We performed extensive testing (achieving 100% coverage), as well as both domain and invariant verifications, to ensure the reliability of the model developed.
To make interaction and user testing with the model easier, Java code that implemented the model was automatically generated using the Overture tool. We then implemented a simple CLI that covers all main functionalities.