
Benedetto Intrigila, Igor Melatti, Alberto Tofani, and Guido Macchiarelli. "Computational models of myocardial endomysial collagen arrangement." Computer Methods and Programs in Biomedicine 86, no. 3 (2007): 232–244. Elsevier NorthHolland, Inc.. ISSN: 01692607. DOI: 10.1016/j.cmpb.2007.03.004.
Abstract: Collagen extracellular matrix is one of the factors related to high passive stiffness of cardiac muscle. However, the architecture and the mechanical aspects of the cardiac collagen matrix are not completely known. In particular, endomysial collagen contribution to the passive mechanics of cardiac muscle as well as its micro anatomical arrangement is still a matter of debate. In order to investigate mechanical and structural properties of endomysial collagen, we consider two alternative computational models of some specific aspects of the cardiac muscle. These two models represent two different views of endomysial collagen distribution: (1) the traditional view and (2) a new view suggested by the data obtained from scanning electron microscopy (SEM) in NaOH macerated samples (a method for isolating collagen from the other tissue). We model the myocardial tissue as a net of spring elements representing the cardiomyocytes together with the endomysial collagen distribution. Each element is a viscous elastic spring, characterized by an elastic and a viscous constant. We connect these springs to imitate the interconnections between collagen fibers. Then we apply to the net of springs some external forces of suitable magnitude and direction, obtaining an extension of the net itself. In our setting, the ratio forces magnitude /net extension is intended to model the stress /strain ratio of a microscopical portion of the myocardial tissue. To solve the problem of the correct identification of the values of the different parameters involved, we use an artificial neural network approach. In particular, we use this technique to learn, given a distribution of external forces, the elastic constants of the springs needed to obtain a desired extension as an equilibrium position. Our experimental findings show that, in the model of collagen distribution structured according to the new view, a given stress /strain ratio (of the net of springs, in the sense specified above) is obtained with much smaller (w.r.t. the other model, corresponding to the traditional view) elasticity constants of the springs. This seems to indicate that by an appropriate structure, a given stiffness of the myocardial tissue can be obtained with endomysial collagen fibers of much smaller size.



Giuseppe Della Penna, Daniele Magazzeni, Alberto Tofani, Benedetto Intrigila, Igor Melatti, and Enrico Tronci. "Automatic Synthesis of Robust Numerical Controllers." In Icas '07, 4. IEEE Computer Society, 2007. ISSN: 0769528595. DOI: 10.1109/CONIELECOMP.2007.59.
Abstract: A major problem of numerical controllers is their robustness, i.e. the state read from the plant may not be in the controller table, although it may be close to some states in the table. For continuous systems, this problem is typically handled by interpolation techniques. Unfortunately, when the plant contains both continuous and discrete variables, the interpolation approach does not work well. To cope with this kind of systems, we propose a general methodology that exploits explicit model checking in an innovative way to automatically synthesize a (time) optimal numerical controller from a plant specification and apply an optimized strengthening algorithm only on the most significant states, in order to reach an acceptable robustness degree. We implemented all the algorithms within our CGMurphi tool, an extension of the wellknown CMurphi verifier, and tested the effectiveness of our approach by applying it to the wellknown truck and trailer obstacles avoidance problem.



Federico Mari, and Enrico Tronci. "CEGAR Based Bounded Model Checking of Discrete Time Hybrid Systems." In Hybrid Systems: Computation and Control (HSCC 2007), edited by A. Bemporad, A. Bicchi and G. C. Buttazzo, 399–412. Lecture Notes in Computer Science 4416. Springer, 2007. DOI: 10.1007/9783540714934_32.
Abstract: Many hybrid systems can be conveniently modeled as Piecewise Affine Discrete Time Hybrid Systems PADTHS. As well known Bounded Model Checking (BMC) for such systems comes down to solve a Mixed Integer Linear Programming (MILP) feasibility problem. We present a SAT based BMC algorithm for automatic verification of PADTHSs. Using Counterexample Guided Abstraction Refinement (CEGAR) our algorithm gradually transforms a PADTHS verification problem into larger and larger SAT problems. Our experimental results show that our approach can handle PADTHSs that are more then 50 times larger than those that can be handled using a MILP solver.
Keywords: Model Checking, Abstraction, CEGAR, SAT, Hybrid Systems, DTHS



Enrico Tronci. "Introductory Paper." Sttt 8, no. 45 (2006): 355–358. DOI: 10.1007/s100090050212y.
Abstract: In todayÃ¢â‚¬â„¢s competitive market designing of digital systems (hardware as well as software) faces tremendous challenges. In fact, notwithstanding an ever decreasing project budget, time to market and product lifetime, designers are faced with an ever increasing system complexity and customer expected quality. The above situation calls for better and better formal verification techniques at all steps of the design flow. This special issue is devoted to publishing revised versions of contributions first presented at the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME) held 21Ã‚â€“24 October 2003 in LÃ¢â‚¬â„¢Aquila, Italy. Authors of well regarded papers from CHARMEÃ¢â‚¬â„¢03 were invited to submit to this special issue. All papers included here have been suitably extended and have undergone an independent round of reviewing.



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: 9783000197109.



Novella Bartolini, and Enrico Tronci. "On Optimizing Service Availability of an Internet Based Architecture for Infrastructure Protection." In Cnip., 2006.



Giuseppe Della Penna, Antinisca Di Marco, Benedetto Intrigila, Igor Melatti, and Alfonso Pierantonio. "Interoperability mapping from XML schemas to ER diagrams." Data Knowl. Eng. 59, no. 1 (2006): 166–188. Elsevier Science Publishers B. V.. ISSN: 0169023x. DOI: 10.1016/j.datak.2005.08.002.
Abstract: The eXtensible Markup Language (XML) is a de facto standard on the Internet and is now being used to exchange a variety of data structures. This leads to the problem of efficiently storing, querying and retrieving a great amount of data contained in XML documents. Unfortunately, XML data often need to coexist with historical data. At present, the best solution for storing XML into preexisting data structures is to extract the information from the XML documents and adapt it to the data structuresÃ¢â‚¬â„¢ logical model (e.g., the relational model of a DBMS). In this paper, we introduce a technique called Xere (XML entityÃ‚â€“relationship exchange) to assist the integration of XML data with other data sources. To this aim, we present an algorithm that maps XML schemas into entityÃ‚â€“relationship diagrams, discuss its soundness and completeness and show its implementation in XSLT.



Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci, and Marisa Venturini Zilli. "Finite horizon analysis of Markov Chains with the Mur$\varphi$ verifier." Int. J. Softw. Tools Technol. Transf. 8, no. 4 (2006): 397–409. SpringerVerlag. ISSN: 14332779. DOI: 10.1007/s1000900502167.
Abstract: In this paper we present an explicit diskbased verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. Given a Markov Chain and an integer k (horizon), our algorithm checks whether the probability of reaching an error state in at most k steps is below a given threshold. We present an implementation of our algorithm within a suitable extension of the Mur$\varphi$ verifier. We call the resulting probabilistic model checker FHPMur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$). We present experimental results comparing FHPMur$\varphi$ with (a finite horizon subset of) PRISM, a stateoftheart symbolic model checker for Markov Chains. Our experimental results show that FHPMur$\varphi$ can handle systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems).



Giuseppe Della Penna, Daniele Magazzeni, Alberto Tofani, Benedetto Intrigila, Igor Melatti, and Enrico Tronci. "Automated Generation of Optimal Controllers through Model Checking Techniques." In IcincoIcso, edited by J. AndradeCetto, J.  L. Ferrier, J. M. C. D. Pereira and J. Filipe, 26–33. INSTICC Press, 2006. ISSN: 9728865597. DOI: 10.1007/9783540791423.
Abstract: We present a methodology for the synthesis of controllers, which exploits (explicit) model checking techniques. That is, we can cope with the systematic exploration of a very large state space. This methodology can be applied to systems where other approaches fail. In particular, we can consider systems with an highly nonlinear dynamics and lacking a uniform mathematical description (model). We can also consider situations where the required control action cannot be specified as a local action, and rather a kind of planning is required. Our methodology individuates first a raw optimal controller, then extends it to obtain a more robust one. A case study is presented which considers the well known trucktrailer obstacle avoidance parking problem, in a parking lot with obstacles on it. The complex nonlinear dynamics of the trucktrailer system, within the presence of obstacles, makes the parking problem extremely hard. We show how, by our methodology, we can obtain optimal controllers with different degrees of robustness.



Igor Melatti, Robert Palmer, Geoffrey Sawaya, Yu Yang, Robert Mike Kirby, and Ganesh Gopalakrishnan. "Parallel and Distributed Model Checking in Eddy." In Model Checking Software, 13th International SPIN Workshop, Vienna, Austria, March 30 – April 1, 2006, Proceedings, edited by A. Valmari, 108–125. Lecture Notes in Computer Science 3925. Springer  Verlag, 2006. ISSN: 03029743. ISBN: 9783540331025. DOI: 10.1007/11691617_7.
Abstract: Model checking of safety properties can be scaled up by pooling the CPU and memory resources of multiple computers. As compute clusters containing 100s of nodes, with each node realized using multicore (e.g., 2) CPUs will be widespread, a model checker based on the parallel (shared memory) and distributed (message passing) paradigms will more efficiently use the hardware resources. Such a model checker can be designed by having each node employ two shared memory threads that run on the (typically) two CPUs of a node, with one thread responsible for state generation, and the other for efficient communication, including (i) performing overlapped asynchronous message passing, and (ii) aggregating the states to be sent into larger chunks in order to improve communication network utilization. We present the design details of such a novel model checking architecture called Eddy. We describe the design rationale, details of how the threads interact and yield control, exchange messages, as well as detect termination. We have realized an instance of this architecture for the Murphi modeling language. Called Eddy_Murphi, we report its performance over the number of nodes as well as communication parameters such as those controlling state aggregation. Nearly linear reduction of compute time with increasing number of nodes is observed. Our thread task partition is done in such a way that it is modular, easy to port across different modeling languages, and easy to tune across a variety of platforms.

