The research focuses on defining a formal model in order to represent properties and hyperproperties of complex software systems. Software systems are represented as Finite/Parameterized and semantically Annotated Timed Transition Systems (Finite/Parameterized ATTS). Properties and hyperproperties are represented as indexed and semantically annotated timed temporal logic formulas. The research aims at studying and defining sound and complete model checking algorithms for the finite version of such systems and appropriate cutoff theorems for reducing the parameterized version of such systems into a finite one. Among the results already obtained, a model checking algorithm (called Semantic Model Checker) for Finite semantically Annotated Transition Systems (a subclass of Finite ATTSs) has been defined. The algorithm has been proved to be sound and complete and has been implemented in a tool available at:  http://code.google.com/p/smc4ws/ .
Furthermore, a cutoff theorem for a Parameterized Timed Transition System (a subclass of Parameterized ATTSs) has been proved. This research activity is at the base of the following activities: “Reverse Engineering”, “Semantic Business Processes and Semantic Web Services”, “Agent Oriented Software Engineering”.
|Laboratory SILab at DII|
|Contact Person: Luca Spalazzi|