Abstract: Many software as well digital hardware automatic synthesis methods define the set of implementations meeting the given system specifications with a boolean relation K. In such a context a fundamental step in the software (hardware) synthesis process is finding effective solutions to the functional equation defined by K. This entails finding a (set of) boolean function(s) F (typically represented using OBDDs, Ordered Binary Decision Diagrams) such that: 1) for all x for which K is satisfiable, K(x, F(x)) = 1 holds; 2) the implementation of F is efficient with respect to given implementation parameters such as code size or execution time. While this problem has been widely studied in digital hardware synthesis, little has been done in a software synthesis context. Unfortunately the approaches developed for hardware synthesis cannot be directly used in a software context. This motivates investigation of effective methods to solve the above problem when F has to be implemented with software. In this paper we present an algorithm that, from an OBDD representation for K, generates a C code implementation for F that has the same size as the OBDD for F and a WCET (Worst Case Execution Time) linear in nr, being n = |x| the number of input arguments for functions in F and r the number of functions in F.

Abstract: The automation of power grids by means of supervisory control and data acquisition (SCADA) systems has led to an improvement of power grid operations and functionalities but also to pervasive cyber interdependencies between power grids and telecommunication networks. Many power grid services are increasingly depending upon the adequate functionality of SCADA system which in turn strictly depends on the adequate functionality of its communication infrastructure. We propose to tackle the SCADA risk analysis by means of different and heterogeneous modeling techniques and software tools. We demonstrate the applicability of our approach through a case study on an actual SCADA system for an electrical power distribution grid. The modeling techniques we discuss aim at providing a probabilistic dependability analysis, followed by a worst case analysis in presence of malicious attacks and a real-time performance evaluation.

Abstract: System Level Analysis calls for a language comprehensible to experts with different background and yet precise enough to support meaningful analyses. SysML is emerging as an effective balance between such conflicting goals. In this paper we outline some the results obtained as for SysML based system level functional formal verification by an ESA/ESTEC study, with a collaboration among INTECS and La Sapienza University of Roma. The study focuses on SysML based system level functional requirements techniques.

Abstract: The main obstruction to automatic verification of Finite State Systems is the huge amount of memory required to complete the verification task (state explosion). This motivates research on distributed as well as disk based verification algorithms. In this paper we present a disk based Breadth First Explicit State Space Exploration algorithm as well as an implementation of it within the Mur$\varphi$ verifier. Our algorithm exploits transition locality (i.e. the statistical fact that most transitions lead to unvisited states or to recently visited states) to decrease disk read accesses thus reducing the time overhead due to disk usage. A disk based verification algorithm for Mur$\varphi$ has been already proposed in the literature. To measure the time speed up due to locality exploitation we compared our algorithm with such previously proposed algorithm. Our experimental results show that our disk based verification algorithm is typically more than 10 times faster than such previously proposed disk based verification algorithm. To measure the time overhead due to disk usage we compared our algorithm with RAM based verification using the (standard) Mur$\varphi$ verifier with enough memory to complete the verification task. Our experimental results show that even when using 1/10 of the RAM needed to complete verification, our disk based algorithm is only between 1.4 and 5.3 times (3 times on average) slower than (RAM) Mur$\varphi$ with enough RAM memory to complete the verification task at hand. Using our disk based Mur$\varphi$ we were able to complete verification of a protocol with about $10^9$ reachable states. This would require more than 5 gigabytes of RAM using RAM based Mur$\varphi$.

Abstract: In this paper we present an algorithm to contrast state explosion when using Explicit State Space Exploration to verify protocols. We show experimentally that protocols exhibit transition locality. We present a verification algorithm that exploits transition locality as well as an implementation of it within the Mur$\varphi$ verifier. Our algorithm is compatible with all Breadth First (BF) optimization techniques present in the Mur$\varphi$ verifier and it is by no means a substitute for any of them. In fact, since our algorithm trades space with time, it is typically most useful when one runs out of memory and has already used all other state reduction techniques present in the Mur$\varphi$ verifier. Our experimental results show that using our approach we can typically save more than 40% of RAM with an average time penalty of about 50% when using (Mur$\varphi$) bit compression and 100% when using bit compression and hash compaction.