|
Andrea Bobbio, Ester Ciancamerla, Saverio Di Blasi, Alessandro Iacomini, Federico Mari, Igor Melatti, Michele Minichino, Alessandro Scarlatti, Enrico Tronci, Roberta Terruggia et al. "Risk analysis via heterogeneous models of SCADA interconnecting Power Grids and Telco networks." In Proceedings of Fourth International Conference on Risks and Security of Internet and Systems (CRiSIS), 90–97., 2009. DOI: 10.1109/CRISIS.2009.5411974.
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.
|
|
|
Toni Mancini, Federico Mari, Annalisa Massini, Igor Melatti, and Enrico Tronci. "Simulator Semantics for System Level Formal Verification." In Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2015),., 2015. DOI: 10.4204/EPTCS.193.7.
|
|
|
E. Tronci, T. Mancini, F. Mari, I. Melatti, R. H. Jacobsen, E. Ebeid, S. A. Mikkelsen, M. Prodanovic, J. K. Gruber, and B. Hayes. "SmartHG: Energy Demand Aware Open Services for Smart Grid Intelligent Automation." In Proceedings of the Work in Progress Session of SEAA/DSD 2014., 2014. ISBN: 978-3-902457-40-0.
|
|
|
Toni Mancini, Federico Mari, Annalisa Massini, Igor Melatti, and Enrico Tronci. "SyLVaaS: System Level Formal Verification as a Service." In Proceedings of the 23rd Euromicro International Conference on Parallel, Distributed and Network-based Processing (PDP 2015), special session on Formal Approaches to Parallel and Distributed Systems (4PAD)., 2015. DOI: 10.1109/PDP.2015.119.
|
|
|
T. Mancini, F. Mari, A. Massini, I. Melatti, and E. Tronci. "SyLVaaS: System Level Formal Verification as a Service." Fundamenta Informaticae 149, no. 1-2 (2016): 101–132. DOI: 10.3233/FI-2016-1444.
|
|
|
Giuseppe Della Penna, Benedetto Intrigila, Enrico Tronci, and Marisa Venturini Zilli. "Synchronized Regular Expressions." Electr. Notes Theor. Comput. Sci. 62 (2002): 195–210. Notes: TOSCA 2001, Theory of Concurrency, Higher Order Languages and Types.
Abstract: Text manipulation is one of the most common tasks for everyone using a computer. The increasing number of textual information in electronic format that every computer user collects everyday stresses the need of more powerful tools to interact with texts. Indeed, much work has been done to provide nonprogramming tools that can be useful for the most common text manipulation issues. Regular Expressions (RE), introduced by Kleene, are well–known in the formal language theory. RE received several extensions, depending on the application of interest. In almost all the implementations of RE search algorithms (e.g. the egrep [A] UNIX command, or the Perl [17] language pattern matching constructs) we find backreferences (as defind in [1]), i.e. expressions that make reference to the string matched by a previous subexpression. Generally speaking, it seems that all the kinds of synchronizations between subexpressions in a RE can be very useful when interacting with texts. Therefore, we introduce the Synchronized Regular Expressions (SRE) as a derivation of the Regular Expressions. We use SRE to present a formal study of the already known backreferences extension, and of a new extension proposed by us, which we call the synchronized exponents. Moreover, since we are talking about formalisms that should have a practical utility and can be used in the real world, we have the problem of how to present SRE to the final users. Therefore, in this paper we also propose a user–friendly syntax for SRE to be used in implementations of SRE–powered search algorithms.
|
|
|
Giuseppe Della Penna, Benedetto Intrigila, Enrico Tronci, and Marisa Venturini Zilli. "Synchronized regular expressions." Acta Inf. 39, no. 1 (2003): 31–70.
Abstract: Text manipulation is one of the most common tasks for everyone using a computer. The increasing number of textual information in electronic format that every computer user collects everyday also increases the need of more powerful tools to interact with texts. Indeed, much work has been done to provide simple and versatile tools that can be useful for the most common text manipulation tasks. Regular Expressions (RE), introduced by Kleene, are well known in the formal language theory. RE have been extended in various ways, depending on the application of interest. In almost all the implementations of RE search algorithms (e.g. the egrep [15] UNIX command, or the Perl [20] language pattern matching constructs) we find backreferences, i.e. expressions that make reference to the string matched by a previous subexpression. Generally speaking, it seems that all kinds of synchronizations between subexpressions in a RE can be very useful when interacting with texts. In this paper we introduce the Synchronized Regular Expressions (SRE) as an extension of the Regular Expressions. We use SRE to present a formal study of the already known backreferences extension, and of a new extension proposed by us, which we call the synchronized exponents. Moreover, since we are dealing with formalisms that should have a practical utility and be used in real applications, we have the problem of how to present SRE to the final users. Therefore, in this paper we also propose a user-friendly syntax for SRE to be used in implementations of SRE-powered search algorithms.
|
|
|
Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems." In Computer Aided Verification, edited by T. Touili, B. Cook and P. Jackson, 180–195. Lecture Notes in Computer Science 6174. Springer Berlin / Heidelberg, 2010. DOI: 10.1007/978-3-642-14295-6_20.
Abstract: We present an algorithm that given a Discrete Time Linear Hybrid System returns a correct-by-construction software implementation K for a (near time optimal) robust quantized feedback controller for along with the set of states on which K is guaranteed to work correctly (controllable region). Furthermore, K has a Worst Case Execution Time linear in the number of bits of the quantization schema.
|
|
|
Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "Synthesizing Control Software from Boolean Relations." International Journal on Advances in Software vol. 5, nr 3&4 (2012): 212–223. IARIA. ISSN: 1942-2628.
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 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. Moreover, a formal
proof of the proposed algorithm correctness is
also shown. Finally, we present experimental
results showing effectiveness of the proposed
algorithm.
Keywords: Control Software Synthesis; Embedded Systems; Model Checking
|
|
|
Toni Mancini, Federico Mari, Annalisa Massini, Igor Melatti, and Enrico Tronci. "System Level Formal Verification via Distributed Multi-Core Hardware in the Loop Simulation." In Proc. of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing. IEEE Computer Society, 2014. DOI: 10.1109/PDP.2014.32.
|
|