Titolo:
| Modelling, Simulation and Verification with Shape Calculus |
Relatore:
| Prof. Luca Tesei - Università di Camerino. |
Luogo:
| Aula Turing - Collegio Raffaello (P.zza della Repubblica, 13). |
Orario:
| 16:00 - 18:00. |
Numero di crediti:
| 0.125 CFU |
Vincoli di partecipazione:
| Nessuno. |
Sommario:
|
Shape Calculus is a spatial process algebra that has been conceived for modelling (not only) biological entities. In this calculus every process has a behavior, expressed as a timed process algebra. Associated to the behavior, a process has a geometrical 3D shape. The communication capabilities of processes depend on the associated shape: only colliding processes can communicate and the outcome of the communication can be a binding, i.e., the creation of a composite 3D process, or just a bump. Processes defined in she Shape Calculus can be directly simulated in the BioShape simulator. The simulator is agent-based and distributed. As agents, other aspects can be added to the original 3D processes, e.g., the possibility to perceive the environment and to communicate with global or local services. BioShape also includes verification tools based on abstract interpretation techniques applied to the Shape Calculus. These techniques permit the formal verification of safety properties about the model defined in Shape Calculus. |
Docente di riferimento:
| Prof. Marco Bernardo. |
| Ultima modifica: 01/03/2013 | Approvato da: Presidente CCdL |