News Items - D-MILS Project Website2024-03-28T10:52:11Zhttp://www.d-mils.org/forum?feed=yes&xn_auth=noFinal results available for downloadtag:www.d-mils.org,2015-12-03:6612808:Topic:88042015-12-03T13:36:00.952ZScott Hansenhttp://www.d-mils.org/profile/2fzhlu8fkset3
<p>The final set of reports from the D-MILS project have been made available for download. Click on the Results tab at the top of the website to access the complete list of available reports.</p>
<p>The final set of reports from the D-MILS project have been made available for download. Click on the Results tab at the top of the website to access the complete list of available reports.</p> Paper on HyComp model checker for hybrid systemstag:www.d-mils.org,2015-01-28:6612808:Topic:50582015-01-28T12:26:34.298ZStefano Tonettahttp://www.d-mils.org/profile/StefanoTonetta
<p>The paper "HyComp: an SMT-based Model Checker for Hybrid Systems" by Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta has been accepted for publication in the proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS15). The tool can verify invariant, LTL and other types of properties on a network of hybrid systems.</p>
<p>The paper "HyComp: an SMT-based Model Checker for Hybrid Systems" by Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta has been accepted for publication in the proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS15). The tool can verify invariant, LTL and other types of properties on a network of hybrid systems.</p> International Workshop on MILS: Architecture and Assurance for Secure Systems, Amsterdam, 20 January 2015tag:www.d-mils.org,2014-11-17:6612808:Topic:48382014-11-17T17:16:23.712ZScott Hansenhttp://www.d-mils.org/profile/2fzhlu8fkset3
<p>We are pleased to inform all of those interested in more information concerning D-MILS technologies that there will be a half-day workshop organised at the <a href="http://www.hipeac.net/2015/amsterdam">HiPEAC Conference 2015</a> titled: <i>International Workshop on MILS: Architecture and Assurance for Secure Systems</i></p>
<p>The workshop will be on 20 January 2015 and is being organised jointly with partners from the <a href="http://www.euromils.eu/" target="_blank">EURO-MILS…</a></p>
<p>We are pleased to inform all of those interested in more information concerning D-MILS technologies that there will be a half-day workshop organised at the <a href="http://www.hipeac.net/2015/amsterdam">HiPEAC Conference 2015</a> titled: <i>International Workshop on MILS: Architecture and Assurance for Secure Systems</i></p>
<p>The workshop will be on 20 January 2015 and is being organised jointly with partners from the <a href="http://www.euromils.eu/" target="_blank">EURO-MILS</a> project.</p>
<p>If you would like to present related work please find further details concerning the <a href="http://mils-workshop.euromils.eu" target="_blank">Call for Papers.</a></p>
<p></p> Paper on Model-Based Assurance Casestag:www.d-mils.org,2014-10-24:6612808:Topic:46232014-10-24T11:09:48.642ZRichard Hawkinshttp://www.d-mils.org/profile/RichardHawkins
<p><span>The paper "Weaving an Assurance Case from Design: A Model-Based Approach</span><span>", authored by team members Richard Hawkins and Tim Kelly with colleagues from the University of York, has been accepted at the <a href="http://www.hase2015.org/" target="_blank">IEEE International Symposium on High Assurance Systems Engineering</a>. The paper</span><span> presents a novel model-based approach, developed on the D-MILS project, for the seamless creation of assurance cases from system…</span></p>
<p><span>The paper "Weaving an Assurance Case from Design: A Model-Based Approach</span><span>", authored by team members Richard Hawkins and Tim Kelly with colleagues from the University of York, has been accepted at the <a href="http://www.hase2015.org/" target="_blank">IEEE International Symposium on High Assurance Systems Engineering</a>. The paper</span><span> presents a novel model-based approach, developed on the D-MILS project, for the seamless creation of assurance cases from system models.</span></p> Best Paper Award at FACS 2014tag:www.d-mils.org,2014-09-12:6612808:Topic:41692014-09-12T08:59:16.435ZThomas Nollhttp://www.d-mils.org/profile/ThomasNoll
<p>The paper "<em>Compositional Analysis Using Component-Oriented Interpolation</em>", co-authored by team members Joost-Pieter Katoen and Thomas Noll, has received the Best Paper Award at the <a href="http://facs2014.cs.unibo.it/" target="_blank">11th International Symposium on Formal Aspects of Component Software (FACS 2014)</a>. It presents a novel abstraction technique that exploits the compositionality of a concurrent system consisting of interacting components.</p>
<p>The paper "<em>Compositional Analysis Using Component-Oriented Interpolation</em>", co-authored by team members Joost-Pieter Katoen and Thomas Noll, has received the Best Paper Award at the <a href="http://facs2014.cs.unibo.it/" target="_blank">11th International Symposium on Formal Aspects of Component Software (FACS 2014)</a>. It presents a novel abstraction technique that exploits the compositionality of a concurrent system consisting of interacting components.</p> Paper on the nuXmv Symbolic Model Checkertag:www.d-mils.org,2014-08-04:6612808:Topic:43072014-08-04T10:11:14.254ZStefano Tonettahttp://www.d-mils.org/profile/StefanoTonetta
<p>The paper "The nuXmv Symbolic Model Checker" by Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta has been published in the proceedings of the International Conference on Computer-Aided Verification (CAV 2014). The paper presents the tool nuXmv, which is a key element of the tool framework used in D-MILS for the verification of MILS-AADL models.</p>
<p>The paper "The nuXmv Symbolic Model Checker" by Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta has been published in the proceedings of the International Conference on Computer-Aided Verification (CAV 2014). The paper presents the tool nuXmv, which is a key element of the tool framework used in D-MILS for the verification of MILS-AADL models.</p> Paper on Verifying LTL properties of hybrid systems with K-livenesstag:www.d-mils.org,2014-08-04:6612808:Topic:43052014-08-04T10:07:06.611ZStefano Tonettahttp://www.d-mils.org/profile/StefanoTonetta
<p>The paper "Verifying LTL properties of hybrid systems with K-liveness" by Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta has been published in the proceedings of the International Conference on Computer-Aided Verification (CAV 2014). The paper presents a new algorithm to verify temporal properties of hybrid automata. This algorithm is used in D-MILS to verify functional, real-time and safety properties of MILS-AADL models.</p>
<p>The paper "Verifying LTL properties of hybrid systems with K-liveness" by Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta has been published in the proceedings of the International Conference on Computer-Aided Verification (CAV 2014). The paper presents a new algorithm to verify temporal properties of hybrid automata. This algorithm is used in D-MILS to verify functional, real-time and safety properties of MILS-AADL models.</p> Paper on Compositional Analysis Using Component-Oriented Interpolationtag:www.d-mils.org,2014-07-31:6612808:Topic:43022014-07-31T10:11:56.925ZThomas Nollhttp://www.d-mils.org/profile/ThomasNoll
<p>The paper "<em>Compositional Analysis Using Component-Oriented Interpolation</em>", co-authored by team members Joost-Pieter Katoen and Thomas Noll, has been accepted at the <a href="http://facs2014.cs.unibo.it/" target="_blank">11th International Symposium on Formal Aspects of Component Software (FACS 2014)</a>. It presents a novel abstraction technique that exploits the compositionality of a concurrent system consisting of interacting components.</p>
<p>The paper "<em>Compositional Analysis Using Component-Oriented Interpolation</em>", co-authored by team members Joost-Pieter Katoen and Thomas Noll, has been accepted at the <a href="http://facs2014.cs.unibo.it/" target="_blank">11th International Symposium on Formal Aspects of Component Software (FACS 2014)</a>. It presents a novel abstraction technique that exploits the compositionality of a concurrent system consisting of interacting components.</p> Paper on secBIP, a framework to study information flow security in component-based systemstag:www.d-mils.org,2014-04-14:6612808:Topic:24452014-04-14T09:15:05.072ZMarius Bozgahttp://www.d-mils.org/profile/MariusBozga
<p>The paper "<em>Model-driven Information Flow Security for Component-Based Systems</em>" by UJV/Verimag team members Najah Ben Said, Saddek Bensalem, Marius Bozga in collaboration with Takoua Abdellatif from Sousse University, Tunisia has been published in the proceedings of <a href="http://www.etaps.org/index.php/2014/workshops?id=164" target="_blank">FPS'14 Workshop</a> "<em>From Programs to Systems - The Systems Perspectives in Computing</em>". The paper introduces <em>secBIP</em>, a…</p>
<p>The paper "<em>Model-driven Information Flow Security for Component-Based Systems</em>" by UJV/Verimag team members Najah Ben Said, Saddek Bensalem, Marius Bozga in collaboration with Takoua Abdellatif from Sousse University, Tunisia has been published in the proceedings of <a href="http://www.etaps.org/index.php/2014/workshops?id=164" target="_blank">FPS'14 Workshop</a> "<em>From Programs to Systems - The Systems Perspectives in Computing</em>". The paper introduces <em>secBIP</em>, a formal framework for studying information flow security in component-based systems. Two<br/>variants of non-interference properties are formally introduced (dealing with respectively, events and data) and for both of them, sufficient conditions that ensures and simplifies the automated verification are proposed. More information from the <a href="http://www.springer.com/computer/theoretical+computer+science/book/978-3-642-54847-5" target="_blank">FPS'14 workshop proceedings</a>.</p> Paper on compositional verification presented at TACAS 2014tag:www.d-mils.org,2014-04-14:6612808:Topic:22772014-04-14T09:00:38.260ZMarius Bozgahttp://www.d-mils.org/profile/MariusBozga
<p>The paper "<em>Compositional Invariant Generation for Timed Systems</em>" by UJF/Verimag team members Lacramioara Astefanoaei, Souha Ben Rayana, Saddek Bensalem, Marius Bozga and Jacques Combaz has been presented at <a href="http://www.etaps.org/index.php/2014/tacas/programme" target="_blank">TACAS 2014</a>, in Grenoble, France. The paper presents a novel method for obtaining invariants for timed systems by combining local invariants, computed locally from components, with global…</p>
<p>The paper "<em>Compositional Invariant Generation for Timed Systems</em>" by UJF/Verimag team members Lacramioara Astefanoaei, Souha Ben Rayana, Saddek Bensalem, Marius Bozga and Jacques Combaz has been presented at <a href="http://www.etaps.org/index.php/2014/tacas/programme" target="_blank">TACAS 2014</a>, in Grenoble, France. The paper presents a novel method for obtaining invariants for timed systems by combining local invariants, computed locally from components, with global invariants, derived from the composition glue. The method is fully compositional and avoid the well known state explosion problem in verification. See more details in the <a href="http://link.springer.com/chapter/10.1007%2F978-3-642-54862-8_18" target="_blank">full paper</a>.</p>