|
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
|
|
|
Federico Mari, Igor Melatti, Enrico Tronci, and Alberto Finzi. "A multi-hop advertising discovery and delivering protocol for multi administrative domain MANET." Mobile Information Systems 3, no. 9 (2013): 261–280. IOS Press. ISSN: 1574-017x (Print) 1875-905X (Online). DOI: 10.3233/MIS-130162.
|
|
|
Roberto Gorrieri, Ruggero Lanotte, Andrea Maggiolo-Schettini, Fabio Martinelli, Simone Tini, and Enrico Tronci. "Automated analysis of timed security: a case study on web privacy." International Journal of Information Security 2, no. 3-4 (2004): 168–186. DOI: 10.1007/s10207-004-0037-9.
Abstract: This paper presents a case study on an automated analysis of real-time security models. The case study on a web system (originally proposed by Felten and Schneider) is presented that shows a timing attack on the privacy of browser users. Three different approaches are followed: LH-Timed Automata (analyzed using the model checker HyTech), finite-state automata (analyzed using the model checker NuSMV), and process algebras (analyzed using the model checker CWB-NC). A comparative analysis of these three approaches is given.
|
|
|
Adolfo Piperno, and Enrico Tronci. "Regular Systems of Equations in λ-calculus." Int. J. Found. Comput. Sci. 1, no. 3 (1990): 325–340. DOI: 10.1142/S0129054190000230.
Abstract: Many problems arising in equational theories like Lambda-calculus and Combinatory Logic can be expressed by combinatory equations or systems of equations. However, the solvability problem for an arbitrarily given class of systems is in general undecidable. In this paper we shall focus our attention on a decidable class of systems, which will be called regular systems, and we shall analyse some classical problems and well-known properties of Lambda-calculus that can be described and solved by means of regular systems. The significance of such class will be emphasized showing that for slight extensions of it the solvability problem turns out to be undecidable.
|
|
|
Giuseppe Della Penna, Daniele Magazzeni, Alberto Tofani, Benedetto Intrigila, Igor Melatti, and Enrico Tronci. "Automated Generation Of Optimal Controllers Through Model Checking Techniques." In Informatics in Control Automation and Robotics. Selected Papers from ICINCO 2006, 107–119. Springer, 2008. DOI: 10.1007/978-3-540-79142-3_10.
|
|
|
Giuseppe Della Penna, Alberto Tofani, Marcello Pecorari, Orazio Raparelli, Benedetto Intrigila, Igor Melatti, and Enrico Tronci. "A Case Study on Automated Generation of Integration Tests." In Fdl, 278–284. Ecsi, 2006. ISSN: 978-3-00-019710-9.
|
|
|
Novella Bartolini, and Enrico Tronci. "On Optimizing Service Availability of an Internet Based Architecture for Infrastructure Protection." In Cnip., 2006.
|
|
|
Michele Cecconi, and Enrico Tronci. "Requirements Formalization and Validation for a Telecommunication Equipment Protection Switcher." In Hase. IEEE Computer Society, 2000. ISSN: 0-7695-0927-4. DOI: 10.1109/HASE.2000.895456.
|
|
|
Amedeo Cesta, Alberto Finzi, Simone Fratini, Andrea Orlandini, and Enrico Tronci. "Merging Planning, Scheduling & Verification – A Preliminary Analysis." In In Proc. of 10th ESA Workshop on Advanced Space Technologies for Robotics and Automation (ASTRA)., 2008.
|
|
|
Amedeo Cesta, Alberto Finzi, Simone Fratini, Andrea Orlandini, and Enrico Tronci. "Validation and Verification Issues in a Timeline-based Planning System." In In E-Proc. of ICAPS Workshop on Knowledge Engineering for Planning and Scheduling., 2008.
Abstract: One of the key points to take into account to foster effective introduction of AI planning and scheduling systems in real world is to develop end user trust in the related technologies. Automated planning and scheduling systems often brings solutions to the users which are neither “obviousÃ¢â‚¬Âť nor immediately acceptable for them. This is due to the ability of these tools to take into account quite an amount of temporal and causal constraints and to employ resolution processes often designed to optimize the solution with respect to non trivial evaluation functions. To increase technology trust, the study of tools for verifying and validating plans and schedules produced by AI systems might be instrumental. In general, validation and verification techniques represent a needed complementary technology in developing domain independent architectures for automated problem solving. This paper presents a preliminary report of the issues concerned with the use of two software tools for formal verification of finite state systems to the validation of the solutions produced by MrSPOCK, a recent effort for building a timeline based planning tool in an ESA project.
|
|