Formal Methods & Software Engineering Lab

Topics

Modelli, metodi e tecniche per il progetto, l'implementazione e il testing di sistemi software

l gruppo FM&SE lavora sia per proporre nuovi formalismi di modellazione e tecniche di analisi, sia su come applicare metodi formali ai campi di specifica ed analisi di sistemi complessi. I sistemi oggetto di studio provengono da una vasta gamma di campi di applicazione, compresi i sistemi embedded, applicazioni orientate ai servizi, distribuiti e sistemi autoadattativi, mobili / cloud e sistemi collaborativi sociali, e dispositivi medici. Particolari tecniche impiegate sono Model-driven Engineering ( MDE ) e notazioni come UML e profili UML, Architecture Description Languages, metodi formali basati sullo stato, come le Abstract State Machines, tecniche di validazione e verifica come la simulazione, la validazione basata su scenari e il model checking mediante il toolset ASMETA. Notazioni formali sono applicate anche nel contesto del testing dell’area del combinatorial testing, del test model-based, e della verifica runtime di conformità.

The FM&SE group has worked both on proposing new modelling formalisms and analysis techniques, and on applying formal methods to the fields of specification and analyses of complex systems. The systems under study come from a very broad variety of application domains, including embedded systems, service-oriented applications, distributed and self-adaptive systems, mobile/cloud and social collaborative systems, and medical devices. Particular techniques employed include Model-driven Engineering (MDE) and lightweight Modeling Languages (such as UML and UML profiles), Architecture Description Languages, state-based formal methods such as Abstract State Machines, validation and verification techniques such as basic simulation, scenario-based validation and model checking of the ASMETA toolset. Formal notations are also applied in the context of testing in the field of combinatorial interaction testing, model-based testing, and conformance runtime verification.

People

Collaborators