https://wiki.ercim.eu/wg/MLQA/api.php?action=feedcontributions&user=Nataliya&feedformat=atomERCIM Working Group MLQA - User contributions [en]2024-03-29T01:58:50ZUser contributionsMediaWiki 1.35.13https://wiki.ercim.eu/wg/MLQA/index.php?title=Group_Activities&diff=442Group Activities2012-07-05T14:04:32Z<p>Nataliya: /* Upcoming events */</p>
<hr />
<div>== Upcoming events ==<br />
<span style="color: red;">The fourth annual meeting: [[MLQA 2012]], Edinburgh, UK.</span><br />
<br />
== Past events ==<br />
<br />
[[MLQA 2011|September 2011: MLQA meeting at CONCUR and QEST 2011, Aachen]] (5'th September, 2011)<br />
<br />
[[July 2010: MLQA meeting at FLoC 2010, Edinburgh]] (9'th July, 2010)<br />
<br />
[[March 2009: Kick-Off meeting in York]] (28'th March 2009)<br />
<br />
== Related events ==<br />
<br />
The QAPL workshop at ETAPS in Paphos, 27-28 March, 2010:<br />
http://qav.comlab.ox.ac.uk/qapl10/<br />
<br />
The QAPL summer school in Bertinoro, 21-26 June, 2010:<br />
http://www.sti.uniurb.it/events/sfm10qapl/</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=438TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T15:50:30Z<p>Nataliya: </p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
==CALL FOR PAPERS==<br />
<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
==SCOPE==<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of <br/> semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing <br/> properties (e.g. security, safety, schedulability) and of other quantifiable <br/> properties such as reliability (for hardware components), trustworthiness <br/> (in information security) and resource usage (e.g. worst-case <br/> memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate <br/> quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control <br/> systems, asynchronous hardware, and to any other domain involving <br/> quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving <br/> quantitative aspects, such as those arising in quantum computation, systems <br/> biology, bioinformatics, etc.<br />
<br />
==TOPICS==<br />
<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
==SUBMISSION==<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
<br />
==IMPORTANT DATES==<br />
<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
==EDITORS==<br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=437TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T15:49:53Z<p>Nataliya: </p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
==CALL FOR PAPERS==<br />
<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
==SCOPE==<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of <br/> semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing <br/> properties (e.g. security, safety, schedulability) and of other quantifiable <br/> properties such as reliability (for hardware components), trustworthiness <br/> (in information security) and resource usage (e.g. worst-case <br/> memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate <br/> quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control<br />
<br />
systems, asynchronous hardware, and to any other domain involving<br />
<br />
quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving <br/> quantitative aspects, such as those arising in quantum computation, systems <br/> biology, bioinformatics, etc.<br />
<br />
==TOPICS==<br />
<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
==SUBMISSION==<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
<br />
==IMPORTANT DATES==<br />
<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
==EDITORS==<br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=436TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T15:46:19Z<p>Nataliya: </p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
==CALL FOR PAPERS==<br />
<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
==SCOPE==<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of <br/>semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing properties (e.g. security, safety, schedulability) and of other quantifiable properties such as reliability (for hardware components), trustworthiness (in information security) and resource usage (e.g. worst-case memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control systems, asynchronous hardware, and to any other domain involving quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving quantitative aspects, such as those arising in quantum computation, systems biology, bioinformatics, etc.<br />
<br />
==TOPICS==<br />
<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
==SUBMISSION==<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
<br />
==IMPORTANT DATES==<br />
<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
==EDITORS==<br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=435TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T15:35:10Z<p>Nataliya: /* SCOPE */</p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
==CALL FOR PAPERS==<br />
<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
==SCOPE==<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of<br />
\ \ semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing properties (e.g. security, safety, schedulability) and of other quantifiable properties such as reliability (for hardware components), trustworthiness (in information security) and resource usage (e.g. worst-case memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control systems, asynchronous hardware, and to any other domain involving quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving quantitative aspects, such as those arising in quantum computation, systems biology, bioinformatics, etc.<br />
<br />
==TOPICS==<br />
<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
==SUBMISSION==<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
<br />
==IMPORTANT DATES==<br />
<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
==EDITORS==<br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=434TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T15:34:50Z<p>Nataliya: /* SCOPE */</p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
==CALL FOR PAPERS==<br />
<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
==SCOPE==<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of<br />
semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing properties (e.g. security, safety, schedulability) and of other quantifiable properties such as reliability (for hardware components), trustworthiness (in information security) and resource usage (e.g. worst-case memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control systems, asynchronous hardware, and to any other domain involving quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving quantitative aspects, such as those arising in quantum computation, systems biology, bioinformatics, etc.<br />
<br />
==TOPICS==<br />
<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
==SUBMISSION==<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
<br />
==IMPORTANT DATES==<br />
<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
==EDITORS==<br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=433TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T15:34:30Z<p>Nataliya: /* SCOPE */</p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
==CALL FOR PAPERS==<br />
<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
==SCOPE==<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of<br />
semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing properties (e.g. security, safety, schedulability) and of other quantifiable properties such as reliability (for hardware components), trustworthiness (in information security) and resource usage (e.g. worst-case memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control systems, asynchronous hardware, and to any other domain involving quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving quantitative aspects, such as those arising in quantum computation, systems biology, bioinformatics, etc.<br />
<br />
==TOPICS==<br />
<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
==SUBMISSION==<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
<br />
==IMPORTANT DATES==<br />
<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
==EDITORS==<br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=432TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T15:33:52Z<p>Nataliya: </p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
==CALL FOR PAPERS==<br />
<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
==SCOPE==<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing properties (e.g. security, safety, schedulability) and of other quantifiable properties such as reliability (for hardware components), trustworthiness (in information security) and resource usage (e.g. worst-case memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control systems, asynchronous hardware, and to any other domain involving quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving quantitative aspects, such as those arising in quantum computation, systems biology, bioinformatics, etc.<br />
<br />
<br />
<br />
<br />
==TOPICS==<br />
<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
==SUBMISSION==<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
<br />
==IMPORTANT DATES==<br />
<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
==EDITORS==<br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=431TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T15:33:45Z<p>Nataliya: </p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE on<br />
<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
==CALL FOR PAPERS==<br />
<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
==SCOPE==<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing properties (e.g. security, safety, schedulability) and of other quantifiable properties such as reliability (for hardware components), trustworthiness (in information security) and resource usage (e.g. worst-case memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control systems, asynchronous hardware, and to any other domain involving quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving quantitative aspects, such as those arising in quantum computation, systems biology, bioinformatics, etc.<br />
<br />
<br />
<br />
<br />
==TOPICS==<br />
<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
==SUBMISSION==<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
<br />
==IMPORTANT DATES==<br />
<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
==EDITORS==<br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=430TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T15:33:12Z<p>Nataliya: /* IMPORTANT DATES */</p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE <br />
<br />
on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
==CALL FOR PAPERS==<br />
<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
==SCOPE==<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing properties (e.g. security, safety, schedulability) and of other quantifiable properties such as reliability (for hardware components), trustworthiness (in information security) and resource usage (e.g. worst-case memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control systems, asynchronous hardware, and to any other domain involving quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving quantitative aspects, such as those arising in quantum computation, systems biology, bioinformatics, etc.<br />
<br />
<br />
<br />
<br />
==TOPICS==<br />
<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
==SUBMISSION==<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
<br />
==IMPORTANT DATES==<br />
<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
==EDITORS==<br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=429TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T15:32:53Z<p>Nataliya: /* IMPORTANT DATES */</p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE <br />
<br />
on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
==CALL FOR PAPERS==<br />
<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
==SCOPE==<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing properties (e.g. security, safety, schedulability) and of other quantifiable properties such as reliability (for hardware components), trustworthiness (in information security) and resource usage (e.g. worst-case memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control systems, asynchronous hardware, and to any other domain involving quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving quantitative aspects, such as those arising in quantum computation, systems biology, bioinformatics, etc.<br />
<br />
<br />
<br />
<br />
==TOPICS==<br />
<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
==SUBMISSION==<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
<br />
==IMPORTANT DATES==<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
==EDITORS==<br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=428TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T15:32:44Z<p>Nataliya: /* IMPORTANT DATES */</p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE <br />
<br />
on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
==CALL FOR PAPERS==<br />
<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
==SCOPE==<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing properties (e.g. security, safety, schedulability) and of other quantifiable properties such as reliability (for hardware components), trustworthiness (in information security) and resource usage (e.g. worst-case memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control systems, asynchronous hardware, and to any other domain involving quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving quantitative aspects, such as those arising in quantum computation, systems biology, bioinformatics, etc.<br />
<br />
<br />
<br />
<br />
==TOPICS==<br />
<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
==SUBMISSION==<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
<br />
==IMPORTANT DATES==<br />
<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
==EDITORS==<br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=427TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T15:32:30Z<p>Nataliya: /* EDITORS */</p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE <br />
<br />
on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
==CALL FOR PAPERS==<br />
<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
==SCOPE==<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing properties (e.g. security, safety, schedulability) and of other quantifiable properties such as reliability (for hardware components), trustworthiness (in information security) and resource usage (e.g. worst-case memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control systems, asynchronous hardware, and to any other domain involving quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving quantitative aspects, such as those arising in quantum computation, systems biology, bioinformatics, etc.<br />
<br />
<br />
<br />
<br />
==TOPICS==<br />
<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
==SUBMISSION==<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
<br />
==IMPORTANT DATES==<br />
<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
<br />
<br />
<br />
<br />
==EDITORS==<br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=426TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T15:32:13Z<p>Nataliya: /* EDITORS */</p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE <br />
<br />
on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
==CALL FOR PAPERS==<br />
<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
==SCOPE==<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing properties (e.g. security, safety, schedulability) and of other quantifiable properties such as reliability (for hardware components), trustworthiness (in information security) and resource usage (e.g. worst-case memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control systems, asynchronous hardware, and to any other domain involving quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving quantitative aspects, such as those arising in quantum computation, systems biology, bioinformatics, etc.<br />
<br />
<br />
<br />
<br />
==TOPICS==<br />
<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
==SUBMISSION==<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
<br />
==IMPORTANT DATES==<br />
<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
<br />
<br />
<br />
<br />
==EDITORS==<br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=425TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T15:31:56Z<p>Nataliya: /* EDITORS */</p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE <br />
<br />
on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
==CALL FOR PAPERS==<br />
<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
==SCOPE==<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing properties (e.g. security, safety, schedulability) and of other quantifiable properties such as reliability (for hardware components), trustworthiness (in information security) and resource usage (e.g. worst-case memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control systems, asynchronous hardware, and to any other domain involving quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving quantitative aspects, such as those arising in quantum computation, systems biology, bioinformatics, etc.<br />
<br />
<br />
<br />
<br />
==TOPICS==<br />
<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
==SUBMISSION==<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
<br />
==IMPORTANT DATES==<br />
<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
<br />
<br />
<br />
<br />
==EDITORS==<br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=424TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T15:04:36Z<p>Nataliya: </p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE <br />
<br />
on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
==CALL FOR PAPERS==<br />
<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
==SCOPE==<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing properties (e.g. security, safety, schedulability) and of other quantifiable properties such as reliability (for hardware components), trustworthiness (in information security) and resource usage (e.g. worst-case memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control systems, asynchronous hardware, and to any other domain involving quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving quantitative aspects, such as those arising in quantum computation, systems biology, bioinformatics, etc.<br />
<br />
<br />
<br />
<br />
==TOPICS==<br />
<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
==SUBMISSION==<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
<br />
==IMPORTANT DATES==<br />
<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
<br />
<br />
<br />
<br />
==EDITORS==<br />
<br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=423TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T15:03:25Z<p>Nataliya: </p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE <br />
<br />
on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
==CALL FOR PAPERS==<br />
<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
==SCOPE==<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing properties (e.g. security, safety, schedulability) and of other quantifiable properties such as reliability (for hardware components), trustworthiness (in information security) and resource usage (e.g. worst-case memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control systems, asynchronous hardware, and to any other domain involving quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving quantitative aspects, such as those arising in quantum computation, systems biology, bioinformatics, etc.<br />
<br />
<br />
<br />
<br />
==TOPICS==<br />
<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
==SUBMISSION==<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
<br />
==IMPORTANT DATES==<br />
<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
<br />
<br />
<br />
<br />
==EDITORS==<br />
<br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=422TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T15:02:02Z<p>Nataliya: </p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE <br />
<br />
on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
==CALL FOR PAPERS==<br />
<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
==SCOPE==<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing<br />
<br />
properties (e.g. security, safety, schedulability) and of other quantifiable<br />
<br />
properties such as reliability (for hardware components), trustworthiness<br />
<br />
(in information security) and resource usage (e.g. worst-case<br />
<br />
memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate<br />
<br />
quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control<br />
<br />
systems, asynchronous hardware, and to any other domain involving<br />
<br />
quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving<br />
<br />
quantitative aspects, such as those arising in quantum computation, systems<br />
<br />
biology, bioinformatics, etc.<br />
<br />
<br />
<br />
<br />
==TOPICS==<br />
<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
==SUBMISSION==<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
<br />
==IMPORTANT DATES==<br />
<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
<br />
<br />
<br />
<br />
==EDITORS==<br />
<br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=421TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T14:59:13Z<p>Nataliya: </p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE <br />
<br />
on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
==CALL FOR PAPERS==<br />
<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
==SCOPE==<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of<br />
<br />
semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing<br />
<br />
properties (e.g. security, safety, schedulability) and of other quantifiable<br />
<br />
properties such as reliability (for hardware components), trustworthiness<br />
<br />
(in information security) and resource usage (e.g. worst-case<br />
<br />
memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate<br />
<br />
quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control<br />
<br />
systems, asynchronous hardware, and to any other domain involving<br />
<br />
quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving<br />
<br />
quantitative aspects, such as those arising in quantum computation, systems<br />
<br />
biology, bioinformatics, etc.<br />
<br />
<br />
<br />
<br />
==TOPICS==<br />
<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
==SUBMISSION==<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
<br />
==IMPORTANT DATES==<br />
<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
<br />
<br />
<br />
<br />
==EDITORS==<br />
<br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=420TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T14:57:43Z<p>Nataliya: </p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE <br />
<br />
on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
==CALL FOR PAPERS==<br />
<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
==SCOPE==<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of<br />
<br />
semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing<br />
<br />
properties (e.g. security, safety, schedulability) and of other quantifiable<br />
<br />
properties such as reliability (for hardware components), trustworthiness<br />
<br />
(in information security) and resource usage (e.g. worst-case<br />
<br />
memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate<br />
<br />
quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control<br />
<br />
systems, asynchronous hardware, and to any other domain involving<br />
<br />
quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving<br />
<br />
quantitative aspects, such as those arising in quantum computation, systems<br />
<br />
biology, bioinformatics, etc.<br />
<br />
<br />
<br />
<br />
==TOPICS==<br />
<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
SUBMISSION<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
IMPORTANT DATES<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
EDITORS<br />
<br />
------------------------------------------------------------------------- <br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=419TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T14:56:57Z<p>Nataliya: </p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE <br />
<br />
on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
==CALL FOR PAPERS==<br />
<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
==SCOPE==<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of<br />
<br />
semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing<br />
<br />
properties (e.g. security, safety, schedulability) and of other quantifiable<br />
<br />
properties such as reliability (for hardware components), trustworthiness<br />
<br />
(in information security) and resource usage (e.g. worst-case<br />
<br />
memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate<br />
<br />
quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control<br />
<br />
systems, asynchronous hardware, and to any other domain involving<br />
<br />
quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving<br />
<br />
quantitative aspects, such as those arising in quantum computation, systems<br />
<br />
biology, bioinformatics, etc.<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
TOPICS<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
SUBMISSION<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
IMPORTANT DATES<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
EDITORS<br />
<br />
------------------------------------------------------------------------- <br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=418TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T14:56:27Z<p>Nataliya: </p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE <br />
<br />
on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
==CALL FOR PAPERS==<br />
<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
SCOPE<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of<br />
<br />
semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing<br />
<br />
properties (e.g. security, safety, schedulability) and of other quantifiable<br />
<br />
properties such as reliability (for hardware components), trustworthiness<br />
<br />
(in information security) and resource usage (e.g. worst-case<br />
<br />
memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate<br />
<br />
quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control<br />
<br />
systems, asynchronous hardware, and to any other domain involving<br />
<br />
quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving<br />
<br />
quantitative aspects, such as those arising in quantum computation, systems<br />
<br />
biology, bioinformatics, etc.<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
TOPICS<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
SUBMISSION<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
IMPORTANT DATES<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
EDITORS<br />
<br />
------------------------------------------------------------------------- <br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=417TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T14:56:14Z<p>Nataliya: </p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE <br />
<br />
on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
==CALL FOR PAPERS==<br />
<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
SCOPE<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of<br />
<br />
semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing<br />
<br />
properties (e.g. security, safety, schedulability) and of other quantifiable<br />
<br />
properties such as reliability (for hardware components), trustworthiness<br />
<br />
(in information security) and resource usage (e.g. worst-case<br />
<br />
memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate<br />
<br />
quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control<br />
<br />
systems, asynchronous hardware, and to any other domain involving<br />
<br />
quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving<br />
<br />
quantitative aspects, such as those arising in quantum computation, systems<br />
<br />
biology, bioinformatics, etc.<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
TOPICS<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
SUBMISSION<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
IMPORTANT DATES<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
EDITORS<br />
<br />
------------------------------------------------------------------------- <br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=416TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T14:55:47Z<p>Nataliya: </p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE <br />
<br />
on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
====================<br />
<br />
CALL FOR PAPERS<br />
<br />
====================<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
SCOPE<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of<br />
<br />
semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing<br />
<br />
properties (e.g. security, safety, schedulability) and of other quantifiable<br />
<br />
properties such as reliability (for hardware components), trustworthiness<br />
<br />
(in information security) and resource usage (e.g. worst-case<br />
<br />
memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate<br />
<br />
quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control<br />
<br />
systems, asynchronous hardware, and to any other domain involving<br />
<br />
quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving<br />
<br />
quantitative aspects, such as those arising in quantum computation, systems<br />
<br />
biology, bioinformatics, etc.<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
TOPICS<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
SUBMISSION<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
IMPORTANT DATES<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
EDITORS<br />
<br />
------------------------------------------------------------------------- <br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=415TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T14:13:23Z<p>Nataliya: </p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE <br />
<br />
on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
********************************<br />
<br />
CALL FOR PAPERS<br />
<br />
********************************<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
SCOPE<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of<br />
<br />
semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing<br />
<br />
properties (e.g. security, safety, schedulability) and of other quantifiable<br />
<br />
properties such as reliability (for hardware components), trustworthiness<br />
<br />
(in information security) and resource usage (e.g. worst-case<br />
<br />
memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate<br />
<br />
quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control<br />
<br />
systems, asynchronous hardware, and to any other domain involving<br />
<br />
quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving<br />
<br />
quantitative aspects, such as those arising in quantum computation, systems<br />
<br />
biology, bioinformatics, etc.<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
TOPICS<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
SUBMISSION<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
IMPORTANT DATES<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
EDITORS<br />
<br />
------------------------------------------------------------------------- <br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=TCS_on_Quantitative_Aspects_of_Programming_Languages_and_Systems&diff=414TCS on Quantitative Aspects of Programming Languages and Systems2012-06-27T14:12:45Z<p>Nataliya: Created page with "Special Issue of THEORETICAL COMPUTER SCIENCE on Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12) ---------------------------------------------------…"</p>
<hr />
<div>Special Issue of THEORETICAL COMPUTER SCIENCE<br />
<br />
on<br />
<br />
Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
********************************<br />
<br />
CALL FOR PAPERS<br />
<br />
********************************<br />
<br />
<br />
<br />
We invite the submission of papers on Quantitative Aspects of Programming<br />
<br />
Languages and Systems for publication in a special issue of the Journal of<br />
<br />
Theoretical Computer Science (TCS). In particular we welcome papers which <br />
<br />
are revised versions of the submitted to and presented at the QAPL 2011<br />
<br />
Workshop in Saarbruecken and QAPL 2012 in Tallinn. We will additionally <br />
<br />
also welcome submissions of papers not presented at QAPL, provided they <br />
<br />
fall into the scope of the call.<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
SCOPE<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Quantitative aspects of computation are important and sometimes essential in<br />
<br />
characterising the behaviour and determining the properties of systems. They<br />
<br />
are related to the use of physical quantities (storage space, time, bandwidth,<br />
<br />
etc.) as well as mathematical quantities (e.g. probability and measures for<br />
<br />
reliability, risk and trust). Such quantities play a central role in defining<br />
<br />
both the model of systems (architecture, language design, semantics) and the<br />
<br />
methodologies and tools for the analysis and verification of system<br />
<br />
properties. This special issue will be devoted to research papers which<br />
<br />
discuss the explicit use of quantitative information such as time and<br />
<br />
probabilities either directly in the model or as a tool for the analysis of<br />
<br />
systems. In particular, contributions should focus on<br />
<br />
<br />
<br />
* the design of probabilistic and real-time languages and the definition of<br />
<br />
semantical models for such languages;<br />
<br />
<br />
<br />
* the discussion of methodologies for the analysis of probabilistic and timing<br />
<br />
properties (e.g. security, safety, schedulability) and of other quantifiable<br />
<br />
properties such as reliability (for hardware components), trustworthiness<br />
<br />
(in information security) and resource usage (e.g. worst-case<br />
<br />
memory/stack/cache requirements);<br />
<br />
<br />
<br />
* the probabilistic analysis of systems which do not explicitly incorporate<br />
<br />
quantitative aspects (e.g. performance, reliability and risk analysis);<br />
<br />
<br />
<br />
* applications to safety-critical systems, communication protocols, control<br />
<br />
systems, asynchronous hardware, and to any other domain involving<br />
<br />
quantitative issues.<br />
<br />
<br />
<br />
* the investigation of computational models and paradigms involving<br />
<br />
quantitative aspects, such as those arising in quantum computation, systems<br />
<br />
biology, bioinformatics, etc.<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
TOPICS<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Topics include (but are not limited to) probabilistic, timing and general<br />
<br />
quantitative aspects in:<br />
<br />
<br />
<br />
Language design, language expressiveness, quantitative language extension,<br />
<br />
semantics, logic, verification, automated reasoning, testing, model-checking,<br />
<br />
program analysis, performance analysis, resource analysis, safety, security<br />
<br />
and protocol analysis, risk and hazard analysis, for biological systems,<br />
<br />
quantum languages, information systems, multi-tasking and multi-core systems,<br />
<br />
time-critical systems, embedded systems, coordination models, scheduling<br />
<br />
theory, distributed systems, concurrent systems, etc.<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
SUBMISSION<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Papers should be 20-25 pages long, including appendices, and should be<br />
<br />
formatted according to Elsevier's elsart document style used for articles in<br />
<br />
the Journal of Theoretical Computer Science (see the Guide for Authors at<br />
<br />
http://ees.elsevier.com/tcs).<br />
<br />
<br />
<br />
http://support.elsevier.com/<br />
<br />
<br />
<br />
Submissions are through the Elsevier Editorial System for TCS located at<br />
<br />
http://ees.elsevier.com/tcs/default.asp. To ensure that all manuscripts are<br />
<br />
correctly identified for inclusion into the special issue, please make sure<br />
<br />
you select/specify "SI:TCS_B QAPL 2011/12" when you reach the step in the<br />
<br />
submission process. <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
IMPORTANT DATES<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
* Paper submission: 15 August 2012<br />
<br />
* Notification: 30 November 2012<br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
EDITORS<br />
<br />
------------------------------------------------------------------------- <br />
<br />
<br />
<br />
Gethin Norman<br />
<br />
University of Glasgow, UK<br />
<br />
gethin@dcs.gla.ac.uk<br />
<br />
<br />
<br />
Mieke Massink<br />
<br />
CNR-ISTI, Pisa, Italy<br />
<br />
mieke.massink@isti.cnr.it <br />
<br />
<br />
<br />
Herbert Wiklicky<br />
<br />
Imperial College London, UK<br />
<br />
herbert@doc.ic.ac.uk <br />
<br />
<br />
<br />
-------------------------------------------------------------------------<br />
<br />
<br />
<br />
Further information at http://www.dcs.gla.ac.uk/qapl11/special_issue.html</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=Main_Page&diff=413Main Page2012-06-27T14:12:04Z<p>Nataliya: /* Upcoming events */</p>
<hr />
<div>== ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA) ==<br />
<br />
[[Image:Image002.png|frame]] Models and Logics for Quantitative Analysis are seen as comprising process models analysed using logics for quantitative properties. More specifically, we will<br />
<br />
# consider process models formally described by transition systems, automata or process calculi,<br />
# consider logics for expressing stochastic and continuous properties as well as discrete ones,<br />
# focus on algorithms, theory and tools, and<br />
# study applications with particular emphasis on embedded systems and service oriented systems but will aim at treating also IT guided workflow systems and biological systems.<br />
<br />
The MLQA home page: http://wiki.ercim.eu/wg/MLQA<br />
<br />
The goal of this working group is to create a venue for knowledge sharing in this exciting area, for creating a network also for young researchers, for sharing tools developed within the field, for discussing research directions, and eventually to formulate a European project or network on formal quantitative analysis.<br />
<br />
The working group will be open also to researchers outside of ERCIM (and outside of Europe).<br />
<br />
== Upcoming events ==<br />
<br />
<span style="color: red;">The fourth annual meeting: [[MLQA 2012]], Edinburgh, UK.</span><br />
<br />
CfP: Special Issue of [[TCS on Quantitative Aspects of Programming Languages and Systems]] (QAPL 2011/12)<br />
<br />
The fifth annual meeting: [[MLQA 2013]], Rome, Italy.<br />
<br />
== Past events ==<br />
<br />
The Kick-Off meeting: [[MLQA 2009|MLQA 2009]], York, UK.<br />
<br />
The second annual meeting: [[MLQA 2010|MLQA 2010]], Edinburgh, UK.<br />
<br />
The third annual meeting: [[MLQA 2011|MLQA 2011]], Aachen, Germany.</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=Main_Page&diff=412Main Page2012-06-27T13:49:21Z<p>Nataliya: /* Upcoming events */</p>
<hr />
<div>== ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA) ==<br />
<br />
[[Image:Image002.png|frame]] Models and Logics for Quantitative Analysis are seen as comprising process models analysed using logics for quantitative properties. More specifically, we will<br />
<br />
# consider process models formally described by transition systems, automata or process calculi,<br />
# consider logics for expressing stochastic and continuous properties as well as discrete ones,<br />
# focus on algorithms, theory and tools, and<br />
# study applications with particular emphasis on embedded systems and service oriented systems but will aim at treating also IT guided workflow systems and biological systems.<br />
<br />
The MLQA home page: http://wiki.ercim.eu/wg/MLQA<br />
<br />
The goal of this working group is to create a venue for knowledge sharing in this exciting area, for creating a network also for young researchers, for sharing tools developed within the field, for discussing research directions, and eventually to formulate a European project or network on formal quantitative analysis.<br />
<br />
The working group will be open also to researchers outside of ERCIM (and outside of Europe).<br />
<br />
== Upcoming events ==<br />
<br />
<span style="color: red;">The fourth annual meeting: [[MLQA 2012]], Edinburgh, UK.</span><br />
<br />
CfP: Special Issue of TCS on Quantitative Aspects of Programming Languages and Systems (QAPL 2011/12)<br />
<br />
The fifth annual meeting: [[MLQA 2013]], Rome, Italy.<br />
<br />
== Past events ==<br />
<br />
The Kick-Off meeting: [[MLQA 2009|MLQA 2009]], York, UK.<br />
<br />
The second annual meeting: [[MLQA 2010|MLQA 2010]], Edinburgh, UK.<br />
<br />
The third annual meeting: [[MLQA 2011|MLQA 2011]], Aachen, Germany.</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=Main_Page&diff=306Main Page2010-11-10T10:22:59Z<p>Nataliya: /* Upcoming events */</p>
<hr />
<div>== ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA) ==<br />
<br />
[[Image:Image002.png|frame]] Models and Logics for Quantitative Analysis are seen as comprising process models analysed using logics for quantitative properties. More specifically, we will<br />
<br />
# consider process models formally described by transition systems, automata or process calculi,<br />
# consider logics for expressing stochastic and continuous properties as well as discrete ones,<br />
# focus on algorithms, theory and tools, and<br />
# study applications with particular emphasis on embedded systems and service oriented systems but will aim at treating also IT guided workflow systems and biological systems.<br />
<br />
The MLQA home page: http://wiki.ercim.eu/wg/MLQA<br />
<br />
The goal of this working group is to create a venue for knowledge sharing in this exciting area, for creating a network also for young researchers, for sharing tools developed within the field, for discussing research directions, and eventually to formulate a European project or network on formal quantitative analysis.<br />
<br />
The working group will be open also to researchers outside of ERCIM (and outside of Europe).<br />
<br />
== Upcoming events ==<br />
<br />
The next meeting of MLQA will be held on September 5, 2011 in Aachen - colocated with CONCUR and QEST.<br />
<br />
== Past events ==<br />
<br />
[[MLQA 2009|MLQA 2009]]<br />
<br />
[[MLQA 2010|MLQA 2010]]</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=Main_Page&diff=305Main Page2010-11-10T10:22:38Z<p>Nataliya: </p>
<hr />
<div>== ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA) ==<br />
<br />
[[Image:Image002.png|frame]] Models and Logics for Quantitative Analysis are seen as comprising process models analysed using logics for quantitative properties. More specifically, we will<br />
<br />
# consider process models formally described by transition systems, automata or process calculi,<br />
# consider logics for expressing stochastic and continuous properties as well as discrete ones,<br />
# focus on algorithms, theory and tools, and<br />
# study applications with particular emphasis on embedded systems and service oriented systems but will aim at treating also IT guided workflow systems and biological systems.<br />
<br />
The MLQA home page: http://wiki.ercim.eu/wg/MLQA<br />
<br />
The goal of this working group is to create a venue for knowledge sharing in this exciting area, for creating a network also for young researchers, for sharing tools developed within the field, for discussing research directions, and eventually to formulate a European project or network on formal quantitative analysis.<br />
<br />
The working group will be open also to researchers outside of ERCIM (and outside of Europe).<br />
<br />
== Upcoming events ==<br />
<br />
Next meeting of MLQA will be held on September 5, 2011 in Aachen - colocated with CONCUR and QEST.<br />
<br />
== Past events ==<br />
<br />
[[MLQA 2009|MLQA 2009]]<br />
<br />
[[MLQA 2010|MLQA 2010]]</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2010&diff=304MLQA 20102010-08-23T09:22:07Z<p>Nataliya: </p>
<hr />
<div>The second annual meeting of the MLQA working group took place on Friday July 9'th 2010 as part of FLoC 2010 in Edinburgh (Scotland). The theme of the meeting was:<br />
<br />
* '''Static Analysis versus Model Checking''': similarities, differences, synergies<br />
<br />
The event consisted of a number of '''invited talks''', a [[Poster Session at MLQA 2010|'''poster session''']] and a '''business meeting'''. The purpose of invited talks was to cover some of the historical developments, survey the links established, establish state-of-the-art, identify the problems still worth pursuing and give a perspective on the implications and (novel) applications that can be foreseen. At the poster session mainly the recent research of the participants and the work in progress was being presented. The long-lasting aim of the meeting was to lay the foundations for future research collaborations on challenging research problems.<br />
<br />
--------------------------------------------------<br />
<br />
See [http://wiki.ercim.eu/wg/MLQA/images/2/27/Handout.pdf '''Handout'''] of the meeting and [http://wiki.ercim.eu/wg/MLQA/images/a/a5/MLQA_2010_Minutes.pdf '''Minutes'''] from the business meeting. See [[Poster Session at MLQA 2010]].<br />
<br />
'''Programme for Friday, July 9'th 2010'''<br />
<br />
(You can see the abstracts and slides of the talks by clicking on the talk titles).<br />
<br />
Friday 9.00-10.00<br />
<br />
* Bernhard Steffen. [[Abstracts FLoC 2010#Bernhard Steffen. From the How to the What: Static Analysis via Model Checking. See slides here.| From the How to the What: Static Analysis via Model Checking.]]<br />
* Flemming Nielson. [[Abstracts FLoC 2010#Flemming Nielson. Model Checking is Static Analysis of Modal Logic. See slides here.|Model Checking is Static Analysis of Modal Logic.]]<br />
<br />
Friday 10.00-10.30<br />
<br />
* Coffee & Poster Session<br />
<br />
Friday 10.30-12.30<br />
<br />
* Marta Kwiatkowska. [[Abstracts FLoC 2010#Marta Kwiatkowska. Quantitative Abstraction Refinement. See slides here.|Quantitative Abstraction Refinement.]]<br />
* Joost-Pieter Katoen. [[Abstracts FLoC 2010#Joost-Pieter Katoen. Invariant Generation for Probabilistic Programs. See slides here.|Invariant Generation for Probabilistic Programs.]]<br />
* Arie Gurfinkel. [[Abstracts FLoC 2010#Marsha Chechik and Arie Gurfinkel. Partial Models and Software Model-Checking. See slides here.|Partial Models and Software Model-Checking.]]<br />
* Orna Grumberg. [[Abstracts FLoC 2010#Orna Grumberg. The 2-valued and the 3-Valued Abstraction-Refinement Frameworks in Model Checking. See slides here.|The 2-valued and the 3-Valued Abstraction-Refinement Frameworks in Model Checking.]]<br />
<br />
Friday 12.30-14.00<br />
<br />
* Lunch<br />
<br />
Friday 14.00-15.00<br />
<br />
* David Monniaux. [[Abstracts FLoC 2010#David Monniaux. Policy iteration for static analysis.|Policy iteration for static analysis.]]<br />
* Michael Huth. [[Abstracts FLoC 2010#Michael Huth. From validating quantitative models to generating valid ones. See slides here.|From validating quantitative models to generating valid ones.]]<br />
<br />
Friday 15.00-15.30<br />
<br />
* Coffee & Poster Session<br />
<br />
Friday 15.30-17.00<br />
<br />
* MLQA Business Meeting (open to all attendees) about the future of MLQA and future research collaborations. See [http://wiki.ercim.eu/wg/MLQA/images/a/a5/MLQA_2010_Minutes.pdf '''Minutes'''] taken during the meeting.</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=Abstracts_FLoC_2010&diff=303Abstracts FLoC 20102010-08-23T09:19:04Z<p>Nataliya: </p>
<hr />
<div>__NOTOC__<br />
==Bernhard Steffen. From the How to the What: Static Analysis via Model Checking. See [http://wiki.ercim.eu/wg/MLQA/images/5/51/MLQA-BS.pdf slides] here.==<br />
<br />
Conceptually comparing the notions of Static Analysis and Model<br />
Checking is delicate. Where are the technical differences, in<br />
the use of logics, abstract interpretation, refinement techniques,<br />
fixpoint computation? Or rather in their pragmatics: the one is fast<br />
but often returns 'don't know', whereas the other may not terminate at<br />
all (cf. Patrick Cousot)? It is hard to agree on a borderline,<br />
and, in fact, earlier recongnized differences vanish as we go.<br />
This is a good sign, as it shows that syngery already happens here,<br />
as is also witnessed by the existence of conferences like VMCAI.<br />
The talk will therefore present a personal view, and a success<br />
story based on this understanding.<br />
<br />
==Flemming Nielson. Model Checking is Static Analysis of Modal Logic. See [http://wiki.ercim.eu/wg/MLQA/images/4/4b/MLQA_2010_MCisSA.pdf slides] here.==<br />
<br />
Flow Logic is an approach to the static analysis of programs that has been developed for functional, imperative and object-oriented programming languages and for concurrent, distributed, mobile and cryptographic process calculi. It is often implemented using an efficient differential worklist based solver (the Succinct Solver) working on contraints presented in a stratified version of Alternation-free Least Fixed Point Logic (ALFP).<br />
<br />
In this talk we show how to deal with modal logics; to be specific we show how to deal with modal logics in the families CTL, ACTL and alternation-free modal mu calculus. We prove that we obtain an exact characterisation of the semantics of formulae in the modal logics and that we remain within stratified ALFP. The computational complexity of model checking by means of static analysis is as for classical approaches to model checking.<br />
<br />
Together with the work of Steffen et al this allows us to conclude that the problems of model checking and static analysis are reducible to each other in many cases. This provides further motivation for transferring methods and techniques between these two approaches to verifying and validating programs and systems.<br />
<br />
This is joint work with Hanne Riis Nielson, Fyuyan Zhang and Piotr Filipiuk.<br />
<br />
==Marta Kwiatkowska. Quantitative Abstraction Refinement. See [http://wiki.ercim.eu/wg/MLQA/images/9/96/Marta-mlqa10.pdf slides] here.==<br />
<br />
Probabilistic model checking has established itself as a valuable technique for formal modelling and analysis of systems that exhibit stochastic behaviour. It has been used to study quantitative properties of a wide range of systems, from randomised communication protocols to biological signalling pathways. In practice, however, scalability quickly becomes a major issue and, for large or even infinite-state systems, abstraction is an essential tool. What is needed are automated and efficient methods for constructing such abstractions.<br />
<br />
In non-probabilistic model checking, this is often done using counterexample-guided abstraction-refinement (CEGAR), which takes a simple, coarse abstraction and then repeatedly refines it until it is amenable to model checking. This talk describes recent and ongoing work on quantitative abstraction-refinement techniques, which can be used to automate the process of building abstractions for probabilistic models. This has already been applied to probabilistic verification of software and of real-time systems, where abstraction is essential.<br />
<br />
==Joost-Pieter Katoen. Invariant Generation for Probabilistic Programs. See [http://wiki.ercim.eu/wg/MLQA/images/e/ee/Mlqa10_joost-pieter.pdf slides] here.==<br />
<br />
Model checking probabilistic programs, typically represented as<br />
Markov decision processes, is en vogue. Abstraction-refinement<br />
techniques (a la CEGAR) have been developed and parametric model<br />
checking approaches have recently been suggested. Prototypical<br />
tools support these techniques. Their usage for programs whose<br />
invariants are quantitative, i.e., arithmetic expressions in the<br />
program variables, is however limited. An alternative is to re-<br />
sort to static analysis techniques.<br />
<br />
We present a constraint-based method for automatically generating quantitative invariants for probabilistic programs. We show how<br />
it can be used, in combination with proof-based methods, to verify properties of probabilistic programs that cannot be analysed by<br />
any of currently existing probabilistic model checkers. To our<br />
knowledge, this is the first automated method for quantitative-<br />
invariant generation.<br />
<br />
(Joint work with Larissa Meinicke, Annabelle McIver and Carroll<br />
Morgan.)<br />
<br />
==Arie Gurfinkel. Partial Models and Software Model-Checking. See [http://wiki.ercim.eu/wg/MLQA/images/5/52/Gurfinkel_mlqa2010_6up.pdf slides] here.==<br />
<br />
Partial models combine necessary and possible behaviours in a single<br />
model. Since they encode both over- and under-approximation<br />
of the behavior of the underlying system into a single model, they<br />
allow both verification and falsification of a broad class of properties.<br />
Thus, they are a natural choice for abstraction in model-checking.<br />
<br />
Yasm is the first symbolic software model-checker to integrate partial models<br />
with the Counterexample-Guided Abstraction Refinement (CEGAR) framework.<br />
Yasm can prove and disprove temporal logic properties with equal effectiveness, and its performance is comparable to standard over-approximating model-checkers. <br />
<br />
In this talk, we describe the types of partial models used by Yasm<br />
and highlight some of our recent developments in software model-checking, including proving non-termination (i.e., finding counterexamples to liveness properties) and reasoning about recursive programs.<br />
<br />
==Orna Grumberg. The 2-valued and the 3-Valued Abstraction-Refinement Frameworks in Model Checking. See [http://wiki.ercim.eu/wg/MLQA/images/b/b4/MLQA-9-7.pdf slides] here.==<br />
<br />
Model checking is a widely used technique for automatic verification of hardware and software systems. Significant amount of research in model checking is devoted to extending its scope to larger and even infinite-state systems.<br />
''Abstraction'' is one of the most successful approaches for doing so. It hides some of the irrelevant details of the system, thus resulting in a small (abstract) model whose correct behavior can be checked. Sometimes the abstraction is too coarse and a desired property cannot be checked on the abstract model. In this case, the abstract model is ''refined'' by adding some of the hidden details back.<br />
<br />
In this talk we present two different frameworks for abstraction-refinement in model checking: The 2-valued (CEGAR) and the 3-valued (TVAR) frameworks. We will describe the abstract models and the type of properties that can be verified with those abstractions. We will also show when refinement is needed.<br />
Finally, we will mention some applications of TVAR and try to convince that it is most useful.<br />
<br />
==David Monniaux. Policy iteration for static analysis.==<br />
<br />
Static analysis by abstract interpretation has traditionally computed<br />
over-approximations of least fixed points (loops or recursive functions)<br />
using Kleene iteration accelerated by widening operators. In recent<br />
years, techniques inspired from game theory have been applied to<br />
fixpoint problems in certain abstract domains: min-policy iterations (E.<br />
Goubault's group) and max-policy iterations (H. Seidl's group). We shall<br />
outline these techniques.<br />
<br />
Finally, we shall discuss recent results, obtained with T. Gawlitza,<br />
about the computation of least fixed points from succinct<br />
representations of programs, giving the same precision as explicitly<br />
distinguishing all program paths but with the same exponential<br />
complexity as the coarse analysis that merges program paths (a naive<br />
approach would incur double exponential complexity). The succinct<br />
representation is exploited through SMT-solving.<br />
<br />
We would appreciate insights for possible applications of such<br />
techniques to succinct representations of e.g. probabilistic systems.<br />
<br />
==Michael Huth. From validating quantitative models to generating valid ones. See [http://wiki.ercim.eu/wg/MLQA/images/b/b6/HuthMLQA10Talk.pdf slides] here.==<br />
<br />
Verification techniques for quantitative systems typically require a system model as object of their investigations. Probabilistic model checking is a representative example of this successful approach.<br />
<br />
However, emerging needs and constraints of quantitative systems no longer allow for, or benefit from, a complete decoupling of the development of a system from its a posteriori verification.<br />
<br />
We paint a somewhat personal picture of what this may mean in terms of challenges and opportunities for those who research the construction of valid quantitative systems.<br />
<br />
Go back to [[MLQA 2010|MLQA meeting at FLoC 2010]]</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=File:MLQA-9-7.pdf&diff=302File:MLQA-9-7.pdf2010-08-23T09:16:38Z<p>Nataliya: </p>
<hr />
<div></div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2010&diff=299MLQA 20102010-07-20T12:33:29Z<p>Nataliya: </p>
<hr />
<div>The second annual meeting of the MLQA working group took place on Friday July 9'th 2010 as part of FLoC 2010 in Edinburgh (Scotland). The theme of the meeting was:<br />
<br />
* '''Static Analysis versus Model Checking''': similarities, differences, synergies<br />
<br />
The event consisted of a number of '''invited talks''', a [[Poster Session at MLQA 2010|'''poster session''']] and a '''business meeting'''. The purpose of invited talks was to cover some of the historical developments, survey the links established, establish state-of-the-art, identify the problems still worth pursuing and give a perspective on the implications and (novel) applications that can be foreseen. At the poster session mainly the recent research of the participants and the work in progress was being presented. The long-lasting aim of the meeting was to lay the foundations for future research collaborations on challenging research problems.<br />
<br />
--------------------------------------------------<br />
<br />
See [http://wiki.ercim.eu/wg/MLQA/images/2/27/Handout.pdf '''Handout'''] of the meeting and [http://wiki.ercim.eu/wg/MLQA/images/a/a5/MLQA_2010_Minutes.pdf '''Minutes'''] from the business meeting. See [[Poster Session at MLQA 2010]].<br />
<br />
'''Programme for Friday, July 9'th 2010'''<br />
<br />
(You can see the abstracts and slides of the talks by clicking on the talk titles).<br />
<br />
Friday 9.00-10.00<br />
<br />
* Bernhard Steffen. [[Abstracts FLoC 2010#Bernhard Steffen. From the How to the What: Static Analysis via Model Checking. See slides here.| From the How to the What: Static Analysis via Model Checking.]]<br />
* Flemming Nielson. [[Abstracts FLoC 2010#Flemming Nielson. Model Checking is Static Analysis of Modal Logic. See slides here.|Model Checking is Static Analysis of Modal Logic.]]<br />
<br />
Friday 10.00-10.30<br />
<br />
* Coffee & Poster Session<br />
<br />
Friday 10.30-12.30<br />
<br />
* Marta Kwiatkowska. [[Abstracts FLoC 2010#Marta Kwiatkowska. Quantitative Abstraction Refinement. See slides here.|Quantitative Abstraction Refinement.]]<br />
* Joost-Pieter Katoen. [[Abstracts FLoC 2010#Joost-Pieter Katoen. Invariant Generation for Probabilistic Programs. See slides here.|Invariant Generation for Probabilistic Programs.]]<br />
* Marsha Chechik and Arie Gurfinkel. [[Abstracts FLoC 2010#Marsha Chechik and Arie Gurfinkel. Partial Models and Software Model-Checking. See slides here.|Partial Models and Software Model-Checking.]]<br />
* Orna Grumberg. [[Abstracts FLoC 2010#Orna Grumberg. The 2-valued and the 3-Valued Abstraction-Refinement Frameworks in Model Checking.|The 2-valued and the 3-Valued Abstraction-Refinement Frameworks in Model Checking.]]<br />
<br />
Friday 12.30-14.00<br />
<br />
* Lunch<br />
<br />
Friday 14.00-15.00<br />
<br />
* David Monniaux. [[Abstracts FLoC 2010#David Monniaux. Policy iteration for static analysis.|Policy iteration for static analysis.]]<br />
* Michael Huth. [[Abstracts FLoC 2010#Michael Huth. From validating quantitative models to generating valid ones. See slides here.|From validating quantitative models to generating valid ones.]]<br />
<br />
Friday 15.00-15.30<br />
<br />
* Coffee & Poster Session<br />
<br />
Friday 15.30-17.00<br />
<br />
* MLQA Business Meeting (open to all attendees) about the future of MLQA and future research collaborations. See [http://wiki.ercim.eu/wg/MLQA/images/a/a5/MLQA_2010_Minutes.pdf '''Minutes'''] taken during the meeting.</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2010&diff=298MLQA 20102010-07-20T12:32:12Z<p>Nataliya: </p>
<hr />
<div>The second annual meeting of the MLQA working group took place on Friday July 9'th 2010 as part of FLoC 2010 in Edinburgh (Scotland). The theme of the meeting was:<br />
<br />
* '''Static Analysis versus Model Checking''': similarities, differences, synergies<br />
<br />
The event consisted of a number of '''invited talks''', a [[Poster Session at MLQA 2010|'''poster session''']] and a '''business meeting'''. The purpose of invited talks was to cover some of the historical developments, survey the links established, establish state-of-the-art, identify the problems still worth pursuing and give a perspective on the implications and (novel) applications that can be foreseen. At the poster session mainly the recent research of the participants and the work in progress was being presented. The long-lasting aim of the meeting was to lay the foundations for future research collaborations on challenging research problems.<br />
<br />
--------------------------------------------------<br />
<br />
See [http://wiki.ercim.eu/wg/MLQA/images/2/27/Handout.pdf '''Handout'''] of the meeting and [http://wiki.ercim.eu/wg/MLQA/images/a/a5/MLQA_2010_Minutes.pdf '''Minutes'''] from the business meeting. See [[Poster Session at MLQA 2010]].<br />
<br />
'''Programme for Friday, July 9'th 2010'''<br />
<br />
(You can see the abstracts and slides of the talks by clicking on the talk titles).<br />
<br />
Friday 9.00-10.00<br />
<br />
* Bernhard Steffen. [[Abstracts FLoC 2010#Bernhard Steffen. From the How to the What: Static Analysis via Model Checking. See slides here.| From the How to the What: Static Analysis via Model Checking.]]<br />
* Flemming Nielson. [[Abstracts FLoC 2010#Flemming Nielson. Model Checking is Static Analysis of Modal Logic. See slides here.|Model Checking is Static Analysis of Modal Logic.]]<br />
<br />
Friday 10.00-10.30<br />
<br />
* Coffee & Poster Session<br />
<br />
Friday 10.30-12.30<br />
<br />
* Marta Kwiatkowska. [[Abstracts FLoC 2010#Marta Kwiatkowska. Quantitative Abstraction Refinement. See slides here.|Quantitative Abstraction Refinement.]]<br />
* Joost-Pieter Katoen. [[Abstracts FLoC 2010#Joost-Pieter Katoen. Invariant Generation for Probabilistic Programs. See slides here.|Invariant Generation for Probabilistic Programs.]]<br />
* Marsha Chechik and Arie Gurfinkel. [[Abstracts FLoC 2010#Marsha Chechik and Arie Gurfinkel. Partial Models and Software Model-Checking. See slides here.|Partial Models and Software Model-Checking.]]<br />
* Orna Grumberg. [[Abstracts FLoC 2010#Orna Grumberg. The 2-valued and the 3-Valued Abstraction-Refinement Frameworks in Model Checking.|The 2-valued and the 3-Valued Abstraction-Refinement Frameworks in Model Checking.]]<br />
<br />
Friday 12.30-14.00<br />
<br />
* Lunch<br />
<br />
Friday 14.00-15.00<br />
<br />
* David Monniaux. [[Abstracts FLoC 2010#David Monniaux. Policy iteration for static analysis.|Policy iteration for static analysis.]]<br />
* Michael Huth. [[Abstracts FLoC 2010#Michael Huth. From validating quantitative models to generating valid ones. See slides here.|From validating quantitative models to generating valid ones.]]<br />
<br />
Friday 15.00-15.30<br />
<br />
* Coffee & Poster Session<br />
<br />
Friday 15.30-17.00<br />
<br />
* MLQA Business Meeting (open to all attendees) about the future of MLQA and future research collaborations. The [http://wiki.ercim.eu/wg/MLQA/images/a/a5/MLQA_2010_Minutes.pdf '''Minutes'''] have been taken during the meeting.</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=File:MLQA_2010_Minutes.pdf&diff=297File:MLQA 2010 Minutes.pdf2010-07-20T12:29:43Z<p>Nataliya: </p>
<hr />
<div></div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2010&diff=296MLQA 20102010-07-20T12:27:02Z<p>Nataliya: </p>
<hr />
<div>The second annual meeting of the MLQA working group took place on Friday July 9'th 2010 as part of FLoC 2010 in Edinburgh (Scotland). The theme of the meeting was:<br />
<br />
* '''Static Analysis versus Model Checking''': similarities, differences, synergies<br />
<br />
The event consisted of a number of '''invited talks''', a [[Poster Session at MLQA 2010|'''poster session''']] and a '''business meeting'''. The purpose of invited talks was to cover some of the historical developments, survey the links established, establish state-of-the-art, identify the problems still worth pursuing and give a perspective on the implications and (novel) applications that can be foreseen. At the poster session mainly the recent research of the participants and the work in progress was being presented. The long-lasting aim of the meeting was to lay the foundations for future research collaborations on challenging research problems.<br />
<br />
--------------------------------------------------<br />
<br />
See [http://wiki.ercim.eu/wg/MLQA/images/2/27/Handout.pdf '''Handout'''] of the meeting. See [[Poster Session at MLQA 2010]].<br />
<br />
'''Programme for Friday, July 9'th 2010'''<br />
<br />
(You can see the abstracts and slides of the talks by clicking on the talk titles).<br />
<br />
Friday 9.00-10.00<br />
<br />
* Bernhard Steffen. [[Abstracts FLoC 2010#Bernhard Steffen. From the How to the What: Static Analysis via Model Checking. See slides here.| From the How to the What: Static Analysis via Model Checking.]]<br />
* Flemming Nielson. [[Abstracts FLoC 2010#Flemming Nielson. Model Checking is Static Analysis of Modal Logic. See slides here.|Model Checking is Static Analysis of Modal Logic.]]<br />
<br />
Friday 10.00-10.30<br />
<br />
* Coffee & Poster Session<br />
<br />
Friday 10.30-12.30<br />
<br />
* Marta Kwiatkowska. [[Abstracts FLoC 2010#Marta Kwiatkowska. Quantitative Abstraction Refinement. See slides here.|Quantitative Abstraction Refinement.]]<br />
* Joost-Pieter Katoen. [[Abstracts FLoC 2010#Joost-Pieter Katoen. Invariant Generation for Probabilistic Programs. See slides here.|Invariant Generation for Probabilistic Programs.]]<br />
* Marsha Chechik and Arie Gurfinkel. [[Abstracts FLoC 2010#Marsha Chechik and Arie Gurfinkel. Partial Models and Software Model-Checking. See slides here.|Partial Models and Software Model-Checking.]]<br />
* Orna Grumberg. [[Abstracts FLoC 2010#Orna Grumberg. The 2-valued and the 3-Valued Abstraction-Refinement Frameworks in Model Checking.|The 2-valued and the 3-Valued Abstraction-Refinement Frameworks in Model Checking.]]<br />
<br />
Friday 12.30-14.00<br />
<br />
* Lunch<br />
<br />
Friday 14.00-15.00<br />
<br />
* David Monniaux. [[Abstracts FLoC 2010#David Monniaux. Policy iteration for static analysis.|Policy iteration for static analysis.]]<br />
* Michael Huth. [[Abstracts FLoC 2010#Michael Huth. From validating quantitative models to generating valid ones. See slides here.|From validating quantitative models to generating valid ones.]]<br />
<br />
Friday 15.00-15.30<br />
<br />
* Coffee & Poster Session<br />
<br />
Friday 15.30-17.00<br />
<br />
* MLQA Business Meeting (open to all attendees) about the future of MLQA and future research collaborations</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=MLQA_2010&diff=295MLQA 20102010-07-20T12:26:06Z<p>Nataliya: </p>
<hr />
<div>The second annual meeting of the MLQA working group took place on Friday July 9'th 2010 as part of FLoC 2010 in Edinburgh (Scotland). The theme of the meeting was:<br />
<br />
* '''Static Analysis versus Model Checking''': similarities, differences, synergies<br />
<br />
The event consisted of a number of '''invited talks''', a [[Poster Session at MLQA 2010|'''poster session''']] and a '''business meeting'''. The purpose of invited talks was to cover some of the historical developments, survey the links established, establish state-of-the-art, identify the problems still worth pursuing and give a perspective on the implications and (novel) applications that can be foreseen. At the poster session mainly the recent research of the participants and the work in progress was being presented. The long-lasting aim of the meeting was to lay the foundations for future research collaborations on challenging research problems.<br />
<br />
--------------------------------------------------<br />
<br />
See [http://wiki.ercim.eu/wg/MLQA/images/2/27/Handout.pdf '''Handout'''] of the meeting. See [[Poster Session at MLQA 2010]].<br />
<br />
'''Programme for Friday, July 9'th 2010'''<br />
<br />
(You can see the abstracts and slides of the talks by clicking on the talk titles).<br />
<br />
Friday 9.00-10.00<br />
<br />
* Bernhard Steffen. [[Abstracts FLoC 2010#Bernhard Steffen. From the How to the What: Static Analysis via Model Checking. See slides here.| From the How to the What: Static Analysis via Model Checking.]]<br />
* Flemming Nielson. [[Abstracts FLoC 2010#Flemming Nielson. Model Checking is Static Analysis of Modal Logic.|Model Checking is Static Analysis of Modal Logic.]]<br />
<br />
Friday 10.00-10.30<br />
<br />
* Coffee & Poster Session<br />
<br />
Friday 10.30-12.30<br />
<br />
* Marta Kwiatkowska. [[Abstracts FLoC 2010#Marta Kwiatkowska. Quantitative Abstraction Refinement.|Quantitative Abstraction Refinement.]]<br />
* Joost-Pieter Katoen. [[Abstracts FLoC 2010#Joost-Pieter Katoen. Invariant Generation for Probabilistic Programs.|Invariant Generation for Probabilistic Programs.]]<br />
* Marsha Chechik and Arie Gurfinkel. [[Abstracts FLoC 2010#Marsha Chechik and Arie Gurfinkel. Partial Models and Software Model-Checking.|Partial Models and Software Model-Checking.]]<br />
* Orna Grumberg. [[Abstracts FLoC 2010#Orna Grumberg. The 2-valued and the 3-Valued Abstraction-Refinement Frameworks in Model Checking.|The 2-valued and the 3-Valued Abstraction-Refinement Frameworks in Model Checking.]]<br />
<br />
Friday 12.30-14.00<br />
<br />
* Lunch<br />
<br />
Friday 14.00-15.00<br />
<br />
* David Monniaux. [[Abstracts FLoC 2010#David Monniaux. Policy iteration for static analysis.|Policy iteration for static analysis.]]<br />
* Michael Huth. [[Abstracts FLoC 2010#Michael Huth. From validating quantitative models to generating valid ones.|From validating quantitative models to generating valid ones.]]<br />
<br />
Friday 15.00-15.30<br />
<br />
* Coffee & Poster Session<br />
<br />
Friday 15.30-17.00<br />
<br />
* MLQA Business Meeting (open to all attendees) about the future of MLQA and future research collaborations</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=Poster_Session_at_MLQA_2010&diff=294Poster Session at MLQA 20102010-07-20T12:21:19Z<p>Nataliya: </p>
<hr />
<div>__NOTOC__<br />
We invited posters under two categories:<br />
<br />
* Presentation of recent or on-going work relating to models, logics, tools, and/or applications with respect to discrete, stochastic and/or continuous systems and properties.<br />
<br />
* Overview of the recent research activities of a group, in relation to the themes of MLQA.<br />
<br />
There were 11 poster submissions to the MLQA poster session. Click on a poster title in order to access the correspondent poster submission in the pdf format.<br />
<br />
==Michael Huth, Nir Piterman, Daniel Wagner. [http://wiki.ercim.eu/wg/MLQA/images/1/14/Submission_1.pdf p-Automata Approach to Probabilistic Verification].==<br />
<br />
The poster introduces an automata based approach to the<br />
verification of probabilistic systems. Our so-called<br />
p-automata combine the combinatorial structure of alternating<br />
tree automata with the ability to quantify probabilities of<br />
regular sets of paths. These foundations enable abstraction-based<br />
probabilistic model checking for probabilistic specifications<br />
that subsume Markov chains, PCTL, LTL and CTL* like logics.<br />
<br />
The poster is based on results from "New Foundations for<br />
Discrete-Time Probabilistic Verification" to appear in<br />
Proceedings of QEST 2010.<br />
<br />
== Nataliya Skrypnyuk, Michael Smith. [http://wiki.ercim.eu/wg/MLQA/images/b/b2/Submission_2.pdf Abstractions of Stochastic Process Algebras.] ==<br />
<br />
Stochastic process algebras are compositional modelling languages<br />
that can be used to describe systems whose behaviour evolves<br />
probabilistically over time - from distributed computer systems, to<br />
signalling pathways in cells. Two such languages are Interactive<br />
Markov Chains (IMC), and the Performance Evaluation Process Algebra<br />
(PEPA), which handle synchronisation between model components in<br />
different ways. The semantics of PEPA can be described as a continuous<br />
time Markov chain (CTMC), whereas for IMC it is a continuous time<br />
Markov decision process (CTMDP).<br />
<br />
In both PEPA and IMC, it is very easy to write a model whose state space<br />
is exponentially larger than its description. It is therefore important to<br />
look for ways to abstract such models, so that they can become small<br />
enough to analyse. Importantly, we want to perform the abstraction at<br />
the language level, so that we maintain the compositionality of the model.<br />
In this poster, we illustrate two different approaches to this - abstraction<br />
of IMC using pathway analysis (a type of static analysis), and abstraction<br />
of PEPA using compositional aggregation of states.<br />
<br />
== Igor Cappello and Paola Quaglia. [http://wiki.ercim.eu/wg/MLQA/images/c/cb/Submission_3.pdf Quantitative Assessment of Web Services: Applying SCOWS to a Real-Life Scenario]. ==<br />
<br />
We present an example of application of SCOWS to a real-life scenario<br />
(loan request) developed within the SENSORIA European Project. SCOWS<br />
is a stochastic process algebra tailored for the purpose of<br />
quantitative assessment of Web Services: applying the labelled<br />
semantics to a SCOWS service S, it is possible to derive the Labelled<br />
Transition System (LTS) representing all the possible behaviours of S.<br />
The LTS can then be used to generate a CTMC on which quantitative<br />
model checking can take place.<br />
<br />
In order to automatically derive the LTS and minimize the state space<br />
needed to represent it, we implemented SCOWS_lts, a tool written in<br />
Java whose output can be imported in a model checker (e.g. PRISM) and<br />
used to perform quantitative analysis.<br />
<br />
We report some results obtained assessing the impact of one parameter<br />
(the rate at which a clerk processes the submitted loan request) on<br />
the overall performance of the service.<br />
<br />
== Ender Yüksel, Hanne Riis Nielson, and Flemming Nielson. [http://wiki.ercim.eu/wg/MLQA/images/4/44/Submission_4.pdf High Security at a Low Cost]. ==<br />
<br />
In the future tiny devices with microcontrollers and sensors will be in charge<br />
of numerous activities in our lives. Tracking our energy consumption and CO2<br />
emission, controlling our living conditions, enforcing security, and monitoring<br />
our health will be some examples of their functions These devices will form<br />
wireless networks to communicate with one another, moreover their power<br />
consumption will be very low. It is not hard to predict that our modern society<br />
will depend on the correct operation of these devices, and the security of the<br />
network they are operating.<br />
<br />
Such sensor-based systems, also known as "cyber-physical systems", achieve<br />
security by means of cryptographic protocols. In a simplistic setting where the<br />
power consumption should be minimum and the processing power is limited, it<br />
is more likely that all devices in the network will share the same cryptographic<br />
key. In this study, we are working on the trade-off between two challenges: <br />
"the cryptographic key should be changed frequently to preserve security" and<br />
"the cryptographic key should be changed rarely to save power". We work on the<br />
ZigBee wireless sensor network standard, that offers the advantages of simple<br />
and low resource communication. We model the system as a continuous-time<br />
Markov chain, and analyze it by posing a number of questions shedding light<br />
on its behaviour. The properties we are interested in are expressed in continuous stochastic logic, and probabilistic model checker Prism is used in the analysis.<br />
<br />
== Erik de Vink, Suzana Andova, and Luuk Groenewegen. [http://wiki.ercim.eu/wg/MLQA/images/8/84/Submission_5.pdf Towards Dynamic Adaptation of Probabilistic Systems]. ==<br />
<br />
Dynamic system adaptation is modeled in Paradigm as coordination of<br />
collaborating components. A special component McPal allows for addition<br />
of new behavior, of new constraints and of new control in view of a new<br />
collaboration. McPal gradually adapts the system dynamics. It is shown<br />
that the approach also applies to the probabilistic setting. For a<br />
client-server example, where McPal gradually adds probabilistic behavior<br />
to deterministic components, precise modeling of changing system<br />
dynamics is achieved. This modeling of the transient behavior, spanning<br />
the complete migration range from as-is collaboration to to-be collabo-<br />
ration, serves as a stepping stone for quantitative analysis of the<br />
system during adaptation.<br />
<br />
== Fuyuan Zhang and Piotr Filipiuk. [http://wiki.ercim.eu/wg/MLQA/images/5/5c/Submission_6.pdf Model Checking is Static Analysis]. ==<br />
<br />
The link between model checking and static analysis has been of great interest<br />
to academia for many years. Early work of Bernhard Steffen and David Schmidt<br />
has shown that classic data-flow analysis is an instance of model checking. The<br />
poster gives an overview of our research aiming to show that also model checking<br />
is static analysis of modal logics and that model checking can be carried by the<br />
static analysis engine; namely ALFP suite. We use Flow Logic, which is a<br />
state-of-the-art approach to static analysis that bridges the gap between a number of approaches to static analysis including Data Flow Analysis, Constraint Based Analysis, Abstract Interpretation and Type and Effect Systems. In the developments it has been demonstrated that Flow Logic is a robust approach that is able to deal with a variety of calculi, programming languages and recently modal logics such as CTL, ACTL and alternation-free mu-calculus. In order to calculate the analysis solution, we use ALFP Suite that computes the least model guaranteed by the Moore family theorem for ALFP. In its current version, the suite supports two solvers, one being a differential worklist solver that is based on a representation of relations as prefix trees and the other being a solver in continuation passing style that is based on a BDD representation of relations.<br />
<br />
== Vashti Galpin, Jane Hillston, and Luca Bortolussi. [http://wiki.ercim.eu/wg/MLQA/images/8/83/Submission_7.pdf A Stochastic Hybrid Process Algebra]. ==<br />
<br />
The process algebra HYPE was developed to model hybrid systems which are<br />
those systems that exhibit both discrete and continuous behaviour. Our new<br />
process algebra extends HYPE by including the ability to model stochastic<br />
behaviour.<br />
<br />
The poster will introduce stochastic HYPE, minimising notational overhead and<br />
through the use of a networking example. It will also contain graphs describing<br />
the evolution of the example over time based on stochastic simulation.<br />
<br />
== David Cachera, Thomas Jensen, Arnaud Jobin, and Pascal Sotin. [http://wiki.ercim.eu/wg/MLQA/images/1/12/Submission_8.pdf A Linear Operator Framework for Analysing Resource Usage]. ==<br />
<br />
We present a semantics-based framework for analysing the quantitative<br />
behaviour of programs with regard to resource usage. We start from an<br />
operational semantics in which costs are modelled using a dioid<br />
structure, which generalizes the classical (max,plus) semiring<br />
structure over reals. The dioid structure of costs allows for defining<br />
the quantitative semantics as a linear operator. We then develop an<br />
approximation framework of such a semantics in order to effectively<br />
compute global cost information from the program. We show how this<br />
framework is related to, and thus can benefit from, the theory of<br />
abstract interpretation for analyzing qualitative properties, We focus<br />
on the notion of long-run cost which models the asymptotic average<br />
cost of a program, and show that our abstraction technique provides a<br />
correct approximation of the concrete long-run cost. We illustrate our<br />
approach on an application example devoted to the computation of<br />
energy consumption for a language with complex array operations and<br />
explicit energy modes management.<br />
<br />
== Christoffer Sloth and Rafael Wisniewski. [http://wiki.ercim.eu/wg/MLQA/images/e/eb/Submission_9.pdf Verification of Continuous Dynamical Systems by Timed Automata]. ==<br />
<br />
The poster outlines a method for abstracting continuous dynamical systems by finite<br />
timed automata, which allows automatic verification of continuous systems. The novelty<br />
of the method is that the abstraction is generated from a partition of state space which<br />
is generated by intersecting set-differences of positive invariant sets.<br />
<br />
It is chosen to abstract continuous systems by timed automata, since tools for efficient<br />
verification of such models exist. Additionally, Lyapunov functions are chosen for<br />
generating the partition, because their sub-level sets are positive invariant; hence, it is<br />
possible to determine a priori if the abstraction is sound or complete. Furthermore, for<br />
certain systems it is possible to approximate the reachable set of the continuous system<br />
arbitrarily close by the timed automaton. The structure added to the abstraction by<br />
partitioning the state space by positive invariant sets allows the timed automaton to be<br />
composed of multiple timed automata. This makes it possible to parallelize the verification<br />
process of the timed automaton.<br />
<br />
Some methods require explicit solutions of the differential equations that describe the<br />
continuous dynamics, which are usually unknown. Therefore, the proposed method only<br />
relies on the Lyapunov functions and their derivatives, which can be calculated.<br />
<br />
The proposed abstraction is applied to an example, which illustrates how sound and<br />
complete abstractions are generated.<br />
<br />
== Lei Song, Flemming Nielson, and Bo Friis Nielson. [http://wiki.ercim.eu/wg/MLQA/images/9/94/Submission_10.pdf A Broadcast Based Stochastic Calculus]. ==<br />
<br />
In our current work we give a stochastic calculus based on broadcast communication. Only<br />
broadcast actions are associated with rates while all the reception actions are passive and<br />
assigned with weights. By doing so there is no need to handle synchronisation between<br />
actions with different rates. We also give a label transition system of our calculus from<br />
which we can get a CTMC naturally. We show the usefulness of our calculus by giving<br />
several examples from performance analysis setting such as batch Markovian arrival<br />
process (BMAP), marked markovian arrival process (MMAP) and closed queueing networks.<br />
<br />
== Massimo Callisto De Donato, Flavio Corradini, Maria Rita Di Berardini, Emanuela Merelli, and Luca Tesei. [http://wiki.ercim.eu/wg/MLQA/images/0/00/Submission_11.pdf Tailoring the Shape Calculus for Quantitative Analysis]. ==<br />
<br />
The Shape Calculus, a bio-inspired language, is a non-deterministic calculus in which processes<br />
are composed of a 3D shape moving in a space and of a behaviour. A process behaviour is formally<br />
expressed as a CCS-like process algebra with deterministic time where channels - the active sites -<br />
are particular surfaces of the shape. A site can bind, after a proper collision, to another compatible<br />
channel forming a more complex shape and a new process. Contextually to the introduction of the<br />
Shape Calculus we defined BioShape, an environment in which a network of Shape Calculus processes,<br />
together with more specific information about motion and behaviour, can be simulated. In particular,<br />
we showed that such a tool is suitable for representing a biological phenomenon at different spatial<br />
and temporal scales and can be used to perform in silico experiments.<br />
<br />
Our aim is to complete the Shape Calculus by providing verification techniques at specification level.<br />
The objective is to find the right abstractions and boundaries that permit the application of existing<br />
quantitative model checking or quantitative equivalence checking techniques to the evolution of a<br />
given network of Shape Calculus processes. Also suitable logic languages for specifying the properties<br />
must be identified. In such a way we target to improve Shape Calculus to promote a coupling between<br />
the calculus and the BioShape tool to work in synergy towards the gaining of quantitative information<br />
about simulated environments.<br />
<br />
Go back to [[MLQA 2010|MLQA meeting at FLoC 2010]]</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=Abstracts_FLoC_2010&diff=293Abstracts FLoC 20102010-07-20T12:21:01Z<p>Nataliya: </p>
<hr />
<div>__NOTOC__<br />
==Bernhard Steffen. From the How to the What: Static Analysis via Model Checking. See [http://wiki.ercim.eu/wg/MLQA/images/5/51/MLQA-BS.pdf slides] here.==<br />
<br />
Conceptually comparing the notions of Static Analysis and Model<br />
Checking is delicate. Where are the technical differences, in<br />
the use of logics, abstract interpretation, refinement techniques,<br />
fixpoint computation? Or rather in their pragmatics: the one is fast<br />
but often returns 'don't know', whereas the other may not terminate at<br />
all (cf. Patrick Cousot)? It is hard to agree on a borderline,<br />
and, in fact, earlier recongnized differences vanish as we go.<br />
This is a good sign, as it shows that syngery already happens here,<br />
as is also witnessed by the existence of conferences like VMCAI.<br />
The talk will therefore present a personal view, and a success<br />
story based on this understanding.<br />
<br />
==Flemming Nielson. Model Checking is Static Analysis of Modal Logic. See [http://wiki.ercim.eu/wg/MLQA/images/4/4b/MLQA_2010_MCisSA.pdf slides] here.==<br />
<br />
Flow Logic is an approach to the static analysis of programs that has been developed for functional, imperative and object-oriented programming languages and for concurrent, distributed, mobile and cryptographic process calculi. It is often implemented using an efficient differential worklist based solver (the Succinct Solver) working on contraints presented in a stratified version of Alternation-free Least Fixed Point Logic (ALFP).<br />
<br />
In this talk we show how to deal with modal logics; to be specific we show how to deal with modal logics in the families CTL, ACTL and alternation-free modal mu calculus. We prove that we obtain an exact characterisation of the semantics of formulae in the modal logics and that we remain within stratified ALFP. The computational complexity of model checking by means of static analysis is as for classical approaches to model checking.<br />
<br />
Together with the work of Steffen et al this allows us to conclude that the problems of model checking and static analysis are reducible to each other in many cases. This provides further motivation for transferring methods and techniques between these two approaches to verifying and validating programs and systems.<br />
<br />
This is joint work with Hanne Riis Nielson, Fyuyan Zhang and Piotr Filipiuk.<br />
<br />
==Marta Kwiatkowska. Quantitative Abstraction Refinement. See [http://wiki.ercim.eu/wg/MLQA/images/9/96/Marta-mlqa10.pdf slides] here.==<br />
<br />
Probabilistic model checking has established itself as a valuable technique for formal modelling and analysis of systems that exhibit stochastic behaviour. It has been used to study quantitative properties of a wide range of systems, from randomised communication protocols to biological signalling pathways. In practice, however, scalability quickly becomes a major issue and, for large or even infinite-state systems, abstraction is an essential tool. What is needed are automated and efficient methods for constructing such abstractions.<br />
<br />
In non-probabilistic model checking, this is often done using counterexample-guided abstraction-refinement (CEGAR), which takes a simple, coarse abstraction and then repeatedly refines it until it is amenable to model checking. This talk describes recent and ongoing work on quantitative abstraction-refinement techniques, which can be used to automate the process of building abstractions for probabilistic models. This has already been applied to probabilistic verification of software and of real-time systems, where abstraction is essential.<br />
<br />
==Joost-Pieter Katoen. Invariant Generation for Probabilistic Programs. See [http://wiki.ercim.eu/wg/MLQA/images/e/ee/Mlqa10_joost-pieter.pdf slides] here.==<br />
<br />
Model checking probabilistic programs, typically represented as<br />
Markov decision processes, is en vogue. Abstraction-refinement<br />
techniques (a la CEGAR) have been developed and parametric model<br />
checking approaches have recently been suggested. Prototypical<br />
tools support these techniques. Their usage for programs whose<br />
invariants are quantitative, i.e., arithmetic expressions in the<br />
program variables, is however limited. An alternative is to re-<br />
sort to static analysis techniques.<br />
<br />
We present a constraint-based method for automatically generating quantitative invariants for probabilistic programs. We show how<br />
it can be used, in combination with proof-based methods, to verify properties of probabilistic programs that cannot be analysed by<br />
any of currently existing probabilistic model checkers. To our<br />
knowledge, this is the first automated method for quantitative-<br />
invariant generation.<br />
<br />
(Joint work with Larissa Meinicke, Annabelle McIver and Carroll<br />
Morgan.)<br />
<br />
==Marsha Chechik and Arie Gurfinkel. Partial Models and Software Model-Checking. See [http://wiki.ercim.eu/wg/MLQA/images/5/52/Gurfinkel_mlqa2010_6up.pdf slides] here.==<br />
<br />
Partial models combine necessary and possible behaviours in a single<br />
model. Since they encode both over- and under-approximation<br />
of the behavior of the underlying system into a single model, they<br />
allow both verification and falsification of a broad class of properties.<br />
Thus, they are a natural choice for abstraction in model-checking.<br />
<br />
Yasm is the first symbolic software model-checker to integrate partial models<br />
with the Counterexample-Guided Abstraction Refinement (CEGAR) framework.<br />
Yasm can prove and disprove temporal logic properties with equal effectiveness, and its performance is comparable to standard over-approximating model-checkers. <br />
<br />
In this talk, we describe the types of partial models used by Yasm<br />
and highlight some of our recent developments in software model-checking, including proving non-termination (i.e., finding counterexamples to liveness properties) and reasoning about recursive programs.<br />
<br />
==Orna Grumberg. The 2-valued and the 3-Valued Abstraction-Refinement Frameworks in Model Checking.==<br />
<br />
Model checking is a widely used technique for automatic verification of hardware and software systems. Significant amount of research in model checking is devoted to extending its scope to larger and even infinite-state systems.<br />
''Abstraction'' is one of the most successful approaches for doing so. It hides some of the irrelevant details of the system, thus resulting in a small (abstract) model whose correct behavior can be checked. Sometimes the abstraction is too coarse and a desired property cannot be checked on the abstract model. In this case, the abstract model is ''refined'' by adding some of the hidden details back.<br />
<br />
In this talk we present two different frameworks for abstraction-refinement in model checking: The 2-valued (CEGAR) and the 3-valued (TVAR) frameworks. We will describe the abstract models and the type of properties that can be verified with those abstractions. We will also show when refinement is needed.<br />
Finally, we will mention some applications of TVAR and try to convince that it is most useful.<br />
<br />
==David Monniaux. Policy iteration for static analysis.==<br />
<br />
Static analysis by abstract interpretation has traditionally computed<br />
over-approximations of least fixed points (loops or recursive functions)<br />
using Kleene iteration accelerated by widening operators. In recent<br />
years, techniques inspired from game theory have been applied to<br />
fixpoint problems in certain abstract domains: min-policy iterations (E.<br />
Goubault's group) and max-policy iterations (H. Seidl's group). We shall<br />
outline these techniques.<br />
<br />
Finally, we shall discuss recent results, obtained with T. Gawlitza,<br />
about the computation of least fixed points from succinct<br />
representations of programs, giving the same precision as explicitly<br />
distinguishing all program paths but with the same exponential<br />
complexity as the coarse analysis that merges program paths (a naive<br />
approach would incur double exponential complexity). The succinct<br />
representation is exploited through SMT-solving.<br />
<br />
We would appreciate insights for possible applications of such<br />
techniques to succinct representations of e.g. probabilistic systems.<br />
<br />
==Michael Huth. From validating quantitative models to generating valid ones. See [http://wiki.ercim.eu/wg/MLQA/images/b/b6/HuthMLQA10Talk.pdf slides] here.==<br />
<br />
Verification techniques for quantitative systems typically require a system model as object of their investigations. Probabilistic model checking is a representative example of this successful approach.<br />
<br />
However, emerging needs and constraints of quantitative systems no longer allow for, or benefit from, a complete decoupling of the development of a system from its a posteriori verification.<br />
<br />
We paint a somewhat personal picture of what this may mean in terms of challenges and opportunities for those who research the construction of valid quantitative systems.<br />
<br />
Go back to [[MLQA 2010|MLQA meeting at FLoC 2010]]</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=Poster_Session_at_MLQA_2010&diff=292Poster Session at MLQA 20102010-07-20T12:19:17Z<p>Nataliya: </p>
<hr />
<div>__NOTOC__<br />
We invited posters under two categories:<br />
<br />
* Presentation of recent or on-going work relating to models, logics, tools, and/or applications with respect to discrete, stochastic and/or continuous systems and properties.<br />
<br />
* Overview of the recent research activities of a group, in relation to the themes of MLQA.<br />
<br />
There were 11 poster submissions to the MLQA poster session. Click on a poster title in order to access the correspondent poster submission in the pdf format.<br />
<br />
==Michael Huth, Nir Piterman, Daniel Wagner. [http://wiki.ercim.eu/wg/MLQA/images/1/14/Submission_1.pdf p-Automata Approach to Probabilistic Verification].==<br />
<br />
The poster introduces an automata based approach to the<br />
verification of probabilistic systems. Our so-called<br />
p-automata combine the combinatorial structure of alternating<br />
tree automata with the ability to quantify probabilities of<br />
regular sets of paths. These foundations enable abstraction-based<br />
probabilistic model checking for probabilistic specifications<br />
that subsume Markov chains, PCTL, LTL and CTL* like logics.<br />
<br />
The poster is based on results from "New Foundations for<br />
Discrete-Time Probabilistic Verification" to appear in<br />
Proceedings of QEST 2010.<br />
<br />
== Nataliya Skrypnyuk, Michael Smith. [http://wiki.ercim.eu/wg/MLQA/images/b/b2/Submission_2.pdf Abstractions of Stochastic Process Algebras.] ==<br />
<br />
Stochastic process algebras are compositional modelling languages<br />
that can be used to describe systems whose behaviour evolves<br />
probabilistically over time - from distributed computer systems, to<br />
signalling pathways in cells. Two such languages are Interactive<br />
Markov Chains (IMC), and the Performance Evaluation Process Algebra<br />
(PEPA), which handle synchronisation between model components in<br />
different ways. The semantics of PEPA can be described as a continuous<br />
time Markov chain (CTMC), whereas for IMC it is a continuous time<br />
Markov decision process (CTMDP).<br />
<br />
In both PEPA and IMC, it is very easy to write a model whose state space<br />
is exponentially larger than its description. It is therefore important to<br />
look for ways to abstract such models, so that they can become small<br />
enough to analyse. Importantly, we want to perform the abstraction at<br />
the language level, so that we maintain the compositionality of the model.<br />
In this poster, we illustrate two different approaches to this - abstraction<br />
of IMC using pathway analysis (a type of static analysis), and abstraction<br />
of PEPA using compositional aggregation of states.<br />
<br />
== Igor Cappello and Paola Quaglia. [http://wiki.ercim.eu/wg/MLQA/images/c/cb/Submission_3.pdf Quantitative Assessment of Web Services: Applying SCOWS to a Real-Life Scenario]. ==<br />
<br />
We present an example of application of SCOWS to a real-life scenario<br />
(loan request) developed within the SENSORIA European Project. SCOWS<br />
is a stochastic process algebra tailored for the purpose of<br />
quantitative assessment of Web Services: applying the labelled<br />
semantics to a SCOWS service S, it is possible to derive the Labelled<br />
Transition System (LTS) representing all the possible behaviours of S.<br />
The LTS can then be used to generate a CTMC on which quantitative<br />
model checking can take place.<br />
<br />
In order to automatically derive the LTS and minimize the state space<br />
needed to represent it, we implemented SCOWS_lts, a tool written in<br />
Java whose output can be imported in a model checker (e.g. PRISM) and<br />
used to perform quantitative analysis.<br />
<br />
We report some results obtained assessing the impact of one parameter<br />
(the rate at which a clerk processes the submitted loan request) on<br />
the overall performance of the service.<br />
<br />
== Ender Yüksel, Hanne Riis Nielson, and Flemming Nielson. [http://wiki.ercim.eu/wg/MLQA/images/4/44/Submission_4.pdf High Security at a Low Cost]. ==<br />
<br />
In the future tiny devices with microcontrollers and sensors will be in charge<br />
of numerous activities in our lives. Tracking our energy consumption and CO2<br />
emission, controlling our living conditions, enforcing security, and monitoring<br />
our health will be some examples of their functions These devices will form<br />
wireless networks to communicate with one another, moreover their power<br />
consumption will be very low. It is not hard to predict that our modern society<br />
will depend on the correct operation of these devices, and the security of the<br />
network they are operating.<br />
<br />
Such sensor-based systems, also known as "cyber-physical systems", achieve<br />
security by means of cryptographic protocols. In a simplistic setting where the<br />
power consumption should be minimum and the processing power is limited, it<br />
is more likely that all devices in the network will share the same cryptographic<br />
key. In this study, we are working on the trade-off between two challenges: <br />
"the cryptographic key should be changed frequently to preserve security" and<br />
"the cryptographic key should be changed rarely to save power". We work on the<br />
ZigBee wireless sensor network standard, that offers the advantages of simple<br />
and low resource communication. We model the system as a continuous-time<br />
Markov chain, and analyze it by posing a number of questions shedding light<br />
on its behaviour. The properties we are interested in are expressed in continuous stochastic logic, and probabilistic model checker Prism is used in the analysis.<br />
<br />
== Erik de Vink, Suzana Andova, and Luuk Groenewegen. [http://wiki.ercim.eu/wg/MLQA/images/8/84/Submission_5.pdf Towards Dynamic Adaptation of Probabilistic Systems]. ==<br />
<br />
Dynamic system adaptation is modeled in Paradigm as coordination of<br />
collaborating components. A special component McPal allows for addition<br />
of new behavior, of new constraints and of new control in view of a new<br />
collaboration. McPal gradually adapts the system dynamics. It is shown<br />
that the approach also applies to the probabilistic setting. For a<br />
client-server example, where McPal gradually adds probabilistic behavior<br />
to deterministic components, precise modeling of changing system<br />
dynamics is achieved. This modeling of the transient behavior, spanning<br />
the complete migration range from as-is collaboration to to-be collabo-<br />
ration, serves as a stepping stone for quantitative analysis of the<br />
system during adaptation.<br />
<br />
== Fuyuan Zhang and Piotr Filipiuk. [http://wiki.ercim.eu/wg/MLQA/images/5/5c/Submission_6.pdf Model Checking is Static Analysis]. ==<br />
<br />
The link between model checking and static analysis has been of great interest<br />
to academia for many years. Early work of Bernhard Steffen and David Schmidt<br />
has shown that classic data-flow analysis is an instance of model checking. The<br />
poster gives an overview of our research aiming to show that also model checking<br />
is static analysis of modal logics and that model checking can be carried by the<br />
static analysis engine; namely ALFP suite. We use Flow Logic, which is a<br />
state-of-the-art approach to static analysis that bridges the gap between a number of approaches to static analysis including Data Flow Analysis, Constraint Based Analysis, Abstract Interpretation and Type and Effect Systems. In the developments it has been demonstrated that Flow Logic is a robust approach that is able to deal with a variety of calculi, programming languages and recently modal logics such as CTL, ACTL and alternation-free mu-calculus. In order to calculate the analysis solution, we use ALFP Suite that computes the least model guaranteed by the Moore family theorem for ALFP. In its current version, the suite supports two solvers, one being a differential worklist solver that is based on a representation of relations as prefix trees and the other being a solver in continuation passing style that is based on a BDD representation of relations.<br />
<br />
== Vashti Galpin, Jane Hillston, and Luca Bortolussi. [http://wiki.ercim.eu/wg/MLQA/images/8/83/Submission_7.pdf A Stochastic Hybrid Process Algebra]. ==<br />
<br />
The process algebra HYPE was developed to model hybrid systems which are<br />
those systems that exhibit both discrete and continuous behaviour. Our new<br />
process algebra extends HYPE by including the ability to model stochastic<br />
behaviour.<br />
<br />
The poster will introduce stochastic HYPE, minimising notational overhead and<br />
through the use of a networking example. It will also contain graphs describing<br />
the evolution of the example over time based on stochastic simulation.<br />
<br />
== David Cachera, Thomas Jensen, Arnaud Jobin, and Pascal Sotin. [http://wiki.ercim.eu/wg/MLQA/images/1/12/Submission_8.pdf A Linear Operator Framework for Analysing Resource Usage]. ==<br />
<br />
We present a semantics-based framework for analysing the quantitative<br />
behaviour of programs with regard to resource usage. We start from an<br />
operational semantics in which costs are modelled using a dioid<br />
structure, which generalizes the classical (max,plus) semiring<br />
structure over reals. The dioid structure of costs allows for defining<br />
the quantitative semantics as a linear operator. We then develop an<br />
approximation framework of such a semantics in order to effectively<br />
compute global cost information from the program. We show how this<br />
framework is related to, and thus can benefit from, the theory of<br />
abstract interpretation for analyzing qualitative properties, We focus<br />
on the notion of long-run cost which models the asymptotic average<br />
cost of a program, and show that our abstraction technique provides a<br />
correct approximation of the concrete long-run cost. We illustrate our<br />
approach on an application example devoted to the computation of<br />
energy consumption for a language with complex array operations and<br />
explicit energy modes management.<br />
<br />
== Christoffer Sloth and Rafael Wisniewski. [http://wiki.ercim.eu/wg/MLQA/images/e/eb/Submission_9.pdf Verification of Continuous Dynamical Systems by Timed Automata]. ==<br />
<br />
The poster outlines a method for abstracting continuous dynamical systems by finite<br />
timed automata, which allows automatic verification of continuous systems. The novelty<br />
of the method is that the abstraction is generated from a partition of state space which<br />
is generated by intersecting set-differences of positive invariant sets.<br />
<br />
It is chosen to abstract continuous systems by timed automata, since tools for efficient<br />
verification of such models exist. Additionally, Lyapunov functions are chosen for<br />
generating the partition, because their sub-level sets are positive invariant; hence, it is<br />
possible to determine a priori if the abstraction is sound or complete. Furthermore, for<br />
certain systems it is possible to approximate the reachable set of the continuous system<br />
arbitrarily close by the timed automaton. The structure added to the abstraction by<br />
partitioning the state space by positive invariant sets allows the timed automaton to be<br />
composed of multiple timed automata. This makes it possible to parallelize the verification<br />
process of the timed automaton.<br />
<br />
Some methods require explicit solutions of the differential equations that describe the<br />
continuous dynamics, which are usually unknown. Therefore, the proposed method only<br />
relies on the Lyapunov functions and their derivatives, which can be calculated.<br />
<br />
The proposed abstraction is applied to an example, which illustrates how sound and<br />
complete abstractions are generated.<br />
<br />
== Lei Song, Flemming Nielson, and Bo Friis Nielson. [http://wiki.ercim.eu/wg/MLQA/images/9/94/Submission_10.pdf A Broadcast Based Stochastic Calculus]. ==<br />
<br />
In our current work we give a stochastic calculus based on broadcast communication. Only<br />
broadcast actions are associated with rates while all the reception actions are passive and<br />
assigned with weights. By doing so there is no need to handle synchronisation between<br />
actions with different rates. We also give a label transition system of our calculus from<br />
which we can get a CTMC naturally. We show the usefulness of our calculus by giving<br />
several examples from performance analysis setting such as batch Markovian arrival<br />
process (BMAP), marked markovian arrival process (MMAP) and closed queueing networks.<br />
<br />
== Massimo Callisto De Donato, Flavio Corradini, Maria Rita Di Berardini, Emanuela Merelli, and Luca Tesei. [http://wiki.ercim.eu/wg/MLQA/images/0/00/Submission_11.pdf Tailoring the Shape Calculus for Quantitative Analysis]. ==<br />
<br />
The Shape Calculus, a bio-inspired language, is a non-deterministic calculus in which processes<br />
are composed of a 3D shape moving in a space and of a behaviour. A process behaviour is formally<br />
expressed as a CCS-like process algebra with deterministic time where channels - the active sites -<br />
are particular surfaces of the shape. A site can bind, after a proper collision, to another compatible<br />
channel forming a more complex shape and a new process. Contextually to the introduction of the<br />
Shape Calculus we defined BioShape, an environment in which a network of Shape Calculus processes,<br />
together with more specific information about motion and behaviour, can be simulated. In particular,<br />
we showed that such a tool is suitable for representing a biological phenomenon at different spatial<br />
and temporal scales and can be used to perform in silico experiments.<br />
<br />
Our aim is to complete the Shape Calculus by providing verification techniques at specification level.<br />
The objective is to find the right abstractions and boundaries that permit the application of existing<br />
quantitative model checking or quantitative equivalence checking techniques to the evolution of a<br />
given network of Shape Calculus processes. Also suitable logic languages for specifying the properties<br />
must be identified. In such a way we target to improve Shape Calculus to promote a coupling between<br />
the calculus and the BioShape tool to work in synergy towards the gaining of quantitative information<br />
about simulated environments.<br />
<br />
Go back to [[July 2010: MLQA meeting at FLoC 2010, Edinburgh|MLQA meeting at FLoC 2010]]</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=Poster_Session_at_MLQA_2010&diff=291Poster Session at MLQA 20102010-07-16T13:27:58Z<p>Nataliya: </p>
<hr />
<div>__NOTOC__<br />
We invited posters under two categories:<br />
<br />
* Presentation of recent or on-going work relating to models, logics, tools, and/or applications with respect to discrete, stochastic and/or continuous systems and properties.<br />
<br />
* Overview of the recent research activities of a group, in relation to the themes of MLQA.<br />
<br />
There were 11 poster submissions to the MLQA poster session. Click on a poster title in order to access the correspondent poster submission in the pdf format.<br />
<br />
==Michael Huth, Nir Piterman, Daniel Wagner. [http://wiki.ercim.eu/wg/MLQA/images/1/14/Submission_1.pdf p-Automata Approach to Probabilistic Verification].==<br />
<br />
The poster introduces an automata based approach to the<br />
verification of probabilistic systems. Our so-called<br />
p-automata combine the combinatorial structure of alternating<br />
tree automata with the ability to quantify probabilities of<br />
regular sets of paths. These foundations enable abstraction-based<br />
probabilistic model checking for probabilistic specifications<br />
that subsume Markov chains, PCTL, LTL and CTL* like logics.<br />
<br />
The poster is based on results from "New Foundations for<br />
Discrete-Time Probabilistic Verification" to appear in<br />
Proceedings of QEST 2010.<br />
<br />
== Nataliya Skrypnyuk, Michael Smith. [http://wiki.ercim.eu/wg/MLQA/images/b/b2/Submission_2.pdf Abstractions of Stochastic Process Algebras.] ==<br />
<br />
Stochastic process algebras are compositional modelling languages<br />
that can be used to describe systems whose behaviour evolves<br />
probabilistically over time - from distributed computer systems, to<br />
signalling pathways in cells. Two such languages are Interactive<br />
Markov Chains (IMC), and the Performance Evaluation Process Algebra<br />
(PEPA), which handle synchronisation between model components in<br />
different ways. The semantics of PEPA can be described as a continuous<br />
time Markov chain (CTMC), whereas for IMC it is a continuous time<br />
Markov decision process (CTMDP).<br />
<br />
In both PEPA and IMC, it is very easy to write a model whose state space<br />
is exponentially larger than its description. It is therefore important to<br />
look for ways to abstract such models, so that they can become small<br />
enough to analyse. Importantly, we want to perform the abstraction at<br />
the language level, so that we maintain the compositionality of the model.<br />
In this poster, we illustrate two different approaches to this - abstraction<br />
of IMC using pathway analysis (a type of static analysis), and abstraction<br />
of PEPA using compositional aggregation of states.<br />
<br />
== Igor Cappello and Paola Quaglia. [http://wiki.ercim.eu/wg/MLQA/images/c/cb/Submission_3.pdf Quantitative Assessment of Web Services: Applying SCOWS to a Real-Life Scenario]. ==<br />
<br />
We present an example of application of SCOWS to a real-life scenario<br />
(loan request) developed within the SENSORIA European Project. SCOWS<br />
is a stochastic process algebra tailored for the purpose of<br />
quantitative assessment of Web Services: applying the labelled<br />
semantics to a SCOWS service S, it is possible to derive the Labelled<br />
Transition System (LTS) representing all the possible behaviours of S.<br />
The LTS can then be used to generate a CTMC on which quantitative<br />
model checking can take place.<br />
<br />
In order to automatically derive the LTS and minimize the state space<br />
needed to represent it, we implemented SCOWS_lts, a tool written in<br />
Java whose output can be imported in a model checker (e.g. PRISM) and<br />
used to perform quantitative analysis.<br />
<br />
We report some results obtained assessing the impact of one parameter<br />
(the rate at which a clerk processes the submitted loan request) on<br />
the overall performance of the service.<br />
<br />
== Ender Yüksel, Hanne Riis Nielson, and Flemming Nielson. [http://wiki.ercim.eu/wg/MLQA/images/4/44/Submission_4.pdf High Security at a Low Cost]. ==<br />
<br />
In the future tiny devices with microcontrollers and sensors will be in charge<br />
of numerous activities in our lives. Tracking our energy consumption and CO2<br />
emission, controlling our living conditions, enforcing security, and monitoring<br />
our health will be some examples of their functions These devices will form<br />
wireless networks to communicate with one another, moreover their power<br />
consumption will be very low. It is not hard to predict that our modern society<br />
will depend on the correct operation of these devices, and the security of the<br />
network they are operating.<br />
<br />
Such sensor-based systems, also known as "cyber-physical systems", achieve<br />
security by means of cryptographic protocols. In a simplistic setting where the<br />
power consumption should be minimum and the processing power is limited, it<br />
is more likely that all devices in the network will share the same cryptographic<br />
key. In this study, we are working on the trade-off between two challenges: <br />
"the cryptographic key should be changed frequently to preserve security" and<br />
"the cryptographic key should be changed rarely to save power". We work on the<br />
ZigBee wireless sensor network standard, that offers the advantages of simple<br />
and low resource communication. We model the system as a continuous-time<br />
Markov chain, and analyze it by posing a number of questions shedding light<br />
on its behaviour. The properties we are interested in are expressed in continuous stochastic logic, and probabilistic model checker Prism is used in the analysis.<br />
<br />
== Erik de Vink, Suzana Andova, and Luuk Groenewegen. [http://wiki.ercim.eu/wg/MLQA/images/8/84/Submission_5.pdf Towards Dynamic Adaptation of Probabilistic Systems]. ==<br />
<br />
Dynamic system adaptation is modeled in Paradigm as coordination of<br />
collaborating components. A special component McPal allows for addition<br />
of new behavior, of new constraints and of new control in view of a new<br />
collaboration. McPal gradually adapts the system dynamics. It is shown<br />
that the approach also applies to the probabilistic setting. For a<br />
client-server example, where McPal gradually adds probabilistic behavior<br />
to deterministic components, precise modeling of changing system<br />
dynamics is achieved. This modeling of the transient behavior, spanning<br />
the complete migration range from as-is collaboration to to-be collabo-<br />
ration, serves as a stepping stone for quantitative analysis of the<br />
system during adaptation.<br />
<br />
== Fuyuan Zhang and Piotr Filipiuk. [http://wiki.ercim.eu/wg/MLQA/images/5/5c/Submission_6.pdf Model Checking is Static Analysis]. ==<br />
<br />
The link between model checking and static analysis has been of great interest<br />
to academia for many years. Early work of Bernhard Steffen and David Schmidt<br />
has shown that classic data-flow analysis is an instance of model checking. The<br />
poster gives an overview of our research aiming to show that also model checking<br />
is static analysis of modal logics and that model checking can be carried by the<br />
static analysis engine; namely ALFP suite. We use Flow Logic, which is a<br />
state-of-the-art approach to static analysis that bridges the gap between a number of approaches to static analysis including Data Flow Analysis, Constraint Based Analysis, Abstract Interpretation and Type and Effect Systems. In the developments it has been demonstrated that Flow Logic is a robust approach that is able to deal with a variety of calculi, programming languages and recently modal logics such as CTL, ACTL and alternation-free mu-calculus. In order to calculate the analysis solution, we use ALFP Suite that computes the least model guaranteed by the Moore family theorem for ALFP. In its current version, the suite supports two solvers, one being a differential worklist solver that is based on a representation of relations as prefix trees and the other being a solver in continuation passing style that is based on a BDD representation of relations.<br />
<br />
== Vashti Galpin, Jane Hillston, and Luca Bortolussi. [http://wiki.ercim.eu/wg/MLQA/images/8/83/Submission_7.pdf A Stochastic Hybrid Process Algebra]. ==<br />
<br />
The process algebra HYPE was developed to model hybrid systems which are<br />
those systems that exhibit both discrete and continuous behaviour. Our new<br />
process algebra extends HYPE by including the ability to model stochastic<br />
behaviour.<br />
<br />
The poster will introduce stochastic HYPE, minimising notational overhead and<br />
through the use of a networking example. It will also contain graphs describing<br />
the evolution of the example over time based on stochastic simulation.<br />
<br />
== David Cachera, Thomas Jensen, Arnaud Jobin, and Pascal Sotin. [http://wiki.ercim.eu/wg/MLQA/images/1/12/Submission_8.pdf A Linear Operator Framework for Analysing Resource Usage]. ==<br />
<br />
We present a semantics-based framework for analysing the quantitative<br />
behaviour of programs with regard to resource usage. We start from an<br />
operational semantics in which costs are modelled using a dioid<br />
structure, which generalizes the classical (max,plus) semiring<br />
structure over reals. The dioid structure of costs allows for defining<br />
the quantitative semantics as a linear operator. We then develop an<br />
approximation framework of such a semantics in order to effectively<br />
compute global cost information from the program. We show how this<br />
framework is related to, and thus can benefit from, the theory of<br />
abstract interpretation for analyzing qualitative properties, We focus<br />
on the notion of long-run cost which models the asymptotic average<br />
cost of a program, and show that our abstraction technique provides a<br />
correct approximation of the concrete long-run cost. We illustrate our<br />
approach on an application example devoted to the computation of<br />
energy consumption for a language with complex array operations and<br />
explicit energy modes management.<br />
<br />
== Christoffer Sloth and Rafael Wisniewski. [http://wiki.ercim.eu/wg/MLQA/images/e/eb/Submission_9.pdf Verification of Continuous Dynamical Systems by Timed Automata]. ==<br />
<br />
The poster outlines a method for abstracting continuous dynamical systems by finite<br />
timed automata, which allows automatic verification of continuous systems. The novelty<br />
of the method is that the abstraction is generated from a partition of state space which<br />
is generated by intersecting set-differences of positive invariant sets.<br />
<br />
It is chosen to abstract continuous systems by timed automata, since tools for efficient<br />
verification of such models exist. Additionally, Lyapunov functions are chosen for<br />
generating the partition, because their sub-level sets are positive invariant; hence, it is<br />
possible to determine a priori if the abstraction is sound or complete. Furthermore, for<br />
certain systems it is possible to approximate the reachable set of the continuous system<br />
arbitrarily close by the timed automaton. The structure added to the abstraction by<br />
partitioning the state space by positive invariant sets allows the timed automaton to be<br />
composed of multiple timed automata. This makes it possible to parallelize the verification<br />
process of the timed automaton.<br />
<br />
Some methods require explicit solutions of the differential equations that describe the<br />
continuous dynamics, which are usually unknown. Therefore, the proposed method only<br />
relies on the Lyapunov functions and their derivatives, which can be calculated.<br />
<br />
The proposed abstraction is applied to an example, which illustrates how sound and<br />
complete abstractions are generated.<br />
<br />
== Lei Song, Flemming Nielson, and Bo Friis Nielson. [http://wiki.ercim.eu/wg/MLQA/images/9/94/Submission_10.pdf A Broadcast Based Stochastic Calculus]. ==<br />
<br />
In our current work we give a stochastic calculus based on broadcast communication. Only<br />
broadcast actions are associated with rates while all the reception actions are passive and<br />
assigned with weights. By doing so there is no need to handle synchronisation between<br />
actions with different rates. We also give a label transition system of our calculus from<br />
which we can get a CTMC naturally. We show the usefulness of our calculus by giving<br />
several examples from performance analysis setting such as batch Markovian arrival<br />
process (BMAP), marked markovian arrival process (MMAP) and closed queueing networks.<br />
<br />
== Massimo Callisto De Donato, Flavio Corradini, Maria Rita Di Berardini, Emanuela Merelli, and Luca Tesei. [http://wiki.ercim.eu/wg/MLQA/images/0/00/Submission_11.pdf Tailoring the Shape Calculus for Quantitative Analysis]. ==<br />
<br />
The Shape Calculus, a bio-inspired language, is a non-deterministic calculus in which processes<br />
are composed of a 3D shape moving in a space and of a behaviour. A process behaviour is formally<br />
expressed as a CCS-like process algebra with deterministic time where channels - the active sites -<br />
are particular surfaces of the shape. A site can bind, after a proper collision, to another compatible<br />
channel forming a more complex shape and a new process. Contextually to the introduction of the<br />
Shape Calculus we defined BioShape, an environment in which a network of Shape Calculus processes,<br />
together with more specific information about motion and behaviour, can be simulated. In particular,<br />
we showed that such a tool is suitable for representing a biological phenomenon at different spatial<br />
and temporal scales and can be used to perform in silico experiments.<br />
<br />
Our aim is to complete the Shape Calculus by providing verification techniques at specification level.<br />
The objective is to find the right abstractions and boundaries that permit the application of existing<br />
quantitative model checking or quantitative equivalence checking techniques to the evolution of a<br />
given network of Shape Calculus processes. Also suitable logic languages for specifying the properties<br />
must be identified. In such a way we target to improve Shape Calculus to promote a coupling between<br />
the calculus and the BioShape tool to work in synergy towards the gaining of quantitative information<br />
about simulated environments.</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=Poster_Session_at_MLQA_2010&diff=290Poster Session at MLQA 20102010-07-16T13:26:35Z<p>Nataliya: </p>
<hr />
<div>__NOTOC__<br />
We invited posters under two categories:<br />
<br />
* Presentation of recent or on-going work relating to models, logics, tools, and/or applications with respect to discrete, stochastic and/or continuous systems and properties.<br />
<br />
* Overview of the recent research activities of a group, in relation to the themes of MLQA.<br />
<br />
There were 11 poster submissions to the MLQA poster session. Click on a poster title in order to access the correspondent poster submission in the pdf format.<br />
<br />
==Michael Huth, Nir Piterman, Daniel Wagner. [http://wiki.ercim.eu/wg/MLQA/images/1/14/Submission_1.pdf p-Automata Approach to Probabilistic Verification].==<br />
<br />
The poster introduces an automata based approach to the<br />
verification of probabilistic systems. Our so-called<br />
p-automata combine the combinatorial structure of alternating<br />
tree automata with the ability to quantify probabilities of<br />
regular sets of paths. These foundations enable abstraction-based<br />
probabilistic model checking for probabilistic specifications<br />
that subsume Markov chains, PCTL, LTL and CTL* like logics.<br />
<br />
The poster is based on results from "New Foundations for<br />
Discrete-Time Probabilistic Verification" to appear in<br />
Proceedings of QEST 2010.<br />
<br />
== Nataliya Skrypnyuk, Michael Smith. [http://wiki.ercim.eu/wg/MLQA/images/b/b2/Submission_2.pdf Abstraction of Stochastic Process Algebras.] ==<br />
<br />
Stochastic process algebras are compositional modelling languages<br />
that can be used to describe systems whose behaviour evolves<br />
probabilistically over time - from distributed computer systems, to<br />
signalling pathways in cells. Two such languages are Interactive<br />
Markov Chains (IMC), and the Performance Evaluation Process Algebra<br />
(PEPA), which handle synchronisation between model components in<br />
different ways. The semantics of PEPA can be described as a continuous<br />
time Markov chain (CTMC), whereas for IMC it is a continuous time<br />
Markov decision process (CTMDP).<br />
<br />
In both PEPA and IMC, it is very easy to write a model whose state space<br />
is exponentially larger than its description. It is therefore important to<br />
look for ways to abstract such models, so that they can become small<br />
enough to analyse. Importantly, we want to perform the abstraction at<br />
the language level, so that we maintain the compositionality of the model.<br />
In this poster, we illustrate two different approaches to this - abstraction<br />
of IMC using pathway analysis (a type of static analysis), and abstraction<br />
of PEPA using compositional aggregation of states.<br />
<br />
== Igor Cappello and Paola Quaglia. [http://wiki.ercim.eu/wg/MLQA/images/c/cb/Submission_3.pdf Quantitative Assessment of Web Services: Applying SCOWS to a Real-Life Scenario]. ==<br />
<br />
We present an example of application of SCOWS to a real-life scenario<br />
(loan request) developed within the SENSORIA European Project. SCOWS<br />
is a stochastic process algebra tailored for the purpose of<br />
quantitative assessment of Web Services: applying the labelled<br />
semantics to a SCOWS service S, it is possible to derive the Labelled<br />
Transition System (LTS) representing all the possible behaviours of S.<br />
The LTS can then be used to generate a CTMC on which quantitative<br />
model checking can take place.<br />
<br />
In order to automatically derive the LTS and minimize the state space<br />
needed to represent it, we implemented SCOWS_lts, a tool written in<br />
Java whose output can be imported in a model checker (e.g. PRISM) and<br />
used to perform quantitative analysis.<br />
<br />
We report some results obtained assessing the impact of one parameter<br />
(the rate at which a clerk processes the submitted loan request) on<br />
the overall performance of the service.<br />
<br />
== Ender Yüksel, Hanne Riis Nielson, and Flemming Nielson. [http://wiki.ercim.eu/wg/MLQA/images/4/44/Submission_4.pdf High Security at a Low Cost]. ==<br />
<br />
In the future tiny devices with microcontrollers and sensors will be in charge<br />
of numerous activities in our lives. Tracking our energy consumption and CO2<br />
emission, controlling our living conditions, enforcing security, and monitoring<br />
our health will be some examples of their functions These devices will form<br />
wireless networks to communicate with one another, moreover their power<br />
consumption will be very low. It is not hard to predict that our modern society<br />
will depend on the correct operation of these devices, and the security of the<br />
network they are operating.<br />
<br />
Such sensor-based systems, also known as "cyber-physical systems", achieve<br />
security by means of cryptographic protocols. In a simplistic setting where the<br />
power consumption should be minimum and the processing power is limited, it<br />
is more likely that all devices in the network will share the same cryptographic<br />
key. In this study, we are working on the trade-off between two challenges: <br />
"the cryptographic key should be changed frequently to preserve security" and<br />
"the cryptographic key should be changed rarely to save power". We work on the<br />
ZigBee wireless sensor network standard, that offers the advantages of simple<br />
and low resource communication. We model the system as a continuous-time<br />
Markov chain, and analyze it by posing a number of questions shedding light<br />
on its behaviour. The properties we are interested in are expressed in continuous stochastic logic, and probabilistic model checker Prism is used in the analysis.<br />
<br />
== Erik de Vink, Suzana Andova, and Luuk Groenewegen. [http://wiki.ercim.eu/wg/MLQA/images/8/84/Submission_5.pdf Towards Dynamic Adaptation of Probabilistic Systems]. ==<br />
<br />
Dynamic system adaptation is modeled in Paradigm as coordination of<br />
collaborating components. A special component McPal allows for addition<br />
of new behavior, of new constraints and of new control in view of a new<br />
collaboration. McPal gradually adapts the system dynamics. It is shown<br />
that the approach also applies to the probabilistic setting. For a<br />
client-server example, where McPal gradually adds probabilistic behavior<br />
to deterministic components, precise modeling of changing system<br />
dynamics is achieved. This modeling of the transient behavior, spanning<br />
the complete migration range from as-is collaboration to to-be collabo-<br />
ration, serves as a stepping stone for quantitative analysis of the<br />
system during adaptation.<br />
<br />
== Fuyuan Zhang and Piotr Filipiuk. [http://wiki.ercim.eu/wg/MLQA/images/5/5c/Submission_6.pdf Model Checking is Static Analysis]. ==<br />
<br />
The link between model checking and static analysis has been of great interest<br />
to academia for many years. Early work of Bernhard Steffen and David Schmidt<br />
has shown that classic data-flow analysis is an instance of model checking. The<br />
poster gives an overview of our research aiming to show that also model checking<br />
is static analysis of modal logics and that model checking can be carried by the<br />
static analysis engine; namely ALFP suite. We use Flow Logic, which is a<br />
state-of-the-art approach to static analysis that bridges the gap between a number of approaches to static analysis including Data Flow Analysis, Constraint Based Analysis, Abstract Interpretation and Type and Effect Systems. In the developments it has been demonstrated that Flow Logic is a robust approach that is able to deal with a variety of calculi, programming languages and recently modal logics such as CTL, ACTL and alternation-free mu-calculus. In order to calculate the analysis solution, we use ALFP Suite that computes the least model guaranteed by the Moore family theorem for ALFP. In its current version, the suite supports two solvers, one being a differential worklist solver that is based on a representation of relations as prefix trees and the other being a solver in continuation passing style that is based on a BDD representation of relations.<br />
<br />
== Vashti Galpin, Jane Hillston, and Luca Bortolussi. [http://wiki.ercim.eu/wg/MLQA/images/8/83/Submission_7.pdf A Stochastic Hybrid Process Algebra]. ==<br />
<br />
The process algebra HYPE was developed to model hybrid systems which are<br />
those systems that exhibit both discrete and continuous behaviour. Our new<br />
process algebra extends HYPE by including the ability to model stochastic<br />
behaviour.<br />
<br />
The poster will introduce stochastic HYPE, minimising notational overhead and<br />
through the use of a networking example. It will also contain graphs describing<br />
the evolution of the example over time based on stochastic simulation.<br />
<br />
== David Cachera, Thomas Jensen, Arnaud Jobin, and Pascal Sotin. [http://wiki.ercim.eu/wg/MLQA/images/1/12/Submission_8.pdf A Linear Operator Framework for Analysing Resource Usage]. ==<br />
<br />
We present a semantics-based framework for analysing the quantitative<br />
behaviour of programs with regard to resource usage. We start from an<br />
operational semantics in which costs are modelled using a dioid<br />
structure, which generalizes the classical (max,plus) semiring<br />
structure over reals. The dioid structure of costs allows for defining<br />
the quantitative semantics as a linear operator. We then develop an<br />
approximation framework of such a semantics in order to effectively<br />
compute global cost information from the program. We show how this<br />
framework is related to, and thus can benefit from, the theory of<br />
abstract interpretation for analyzing qualitative properties, We focus<br />
on the notion of long-run cost which models the asymptotic average<br />
cost of a program, and show that our abstraction technique provides a<br />
correct approximation of the concrete long-run cost. We illustrate our<br />
approach on an application example devoted to the computation of<br />
energy consumption for a language with complex array operations and<br />
explicit energy modes management.<br />
<br />
== Christoffer Sloth and Rafael Wisniewski. [http://wiki.ercim.eu/wg/MLQA/images/e/eb/Submission_9.pdf Verification of Continuous Dynamical Systems by Timed Automata]. ==<br />
<br />
The poster outlines a method for abstracting continuous dynamical systems by finite<br />
timed automata, which allows automatic verification of continuous systems. The novelty<br />
of the method is that the abstraction is generated from a partition of state space which<br />
is generated by intersecting set-differences of positive invariant sets.<br />
<br />
It is chosen to abstract continuous systems by timed automata, since tools for efficient<br />
verification of such models exist. Additionally, Lyapunov functions are chosen for<br />
generating the partition, because their sub-level sets are positive invariant; hence, it is<br />
possible to determine a priori if the abstraction is sound or complete. Furthermore, for<br />
certain systems it is possible to approximate the reachable set of the continuous system<br />
arbitrarily close by the timed automaton. The structure added to the abstraction by<br />
partitioning the state space by positive invariant sets allows the timed automaton to be<br />
composed of multiple timed automata. This makes it possible to parallelize the verification<br />
process of the timed automaton.<br />
<br />
Some methods require explicit solutions of the differential equations that describe the<br />
continuous dynamics, which are usually unknown. Therefore, the proposed method only<br />
relies on the Lyapunov functions and their derivatives, which can be calculated.<br />
<br />
The proposed abstraction is applied to an example, which illustrates how sound and<br />
complete abstractions are generated.<br />
<br />
== Lei Song, Flemming Nielson, and Bo Friis Nielson. [http://wiki.ercim.eu/wg/MLQA/images/9/94/Submission_10.pdf A Broadcast Based Stochastic Calculus]. ==<br />
<br />
In our current work we give a stochastic calculus based on broadcast communication. Only<br />
broadcast actions are associated with rates while all the reception actions are passive and<br />
assigned with weights. By doing so there is no need to handle synchronisation between<br />
actions with different rates. We also give a label transition system of our calculus from<br />
which we can get a CTMC naturally. We show the usefulness of our calculus by giving<br />
several examples from performance analysis setting such as batch Markovian arrival<br />
process (BMAP), marked markovian arrival process (MMAP) and closed queueing networks.<br />
<br />
== Massimo Callisto De Donato, Flavio Corradini, Maria Rita Di Berardini, Emanuela Merelli, and Luca Tesei. [http://wiki.ercim.eu/wg/MLQA/images/0/00/Submission_11.pdf Tailoring the Shape Calculus for Quantitative Analysis]. ==<br />
<br />
The Shape Calculus, a bio-inspired language, is a non-deterministic calculus in which processes<br />
are composed of a 3D shape moving in a space and of a behaviour. A process behaviour is formally<br />
expressed as a CCS-like process algebra with deterministic time where channels - the active sites -<br />
are particular surfaces of the shape. A site can bind, after a proper collision, to another compatible<br />
channel forming a more complex shape and a new process. Contextually to the introduction of the<br />
Shape Calculus we defined BioShape, an environment in which a network of Shape Calculus processes,<br />
together with more specific information about motion and behaviour, can be simulated. In particular,<br />
we showed that such a tool is suitable for representing a biological phenomenon at different spatial<br />
and temporal scales and can be used to perform in silico experiments.<br />
<br />
Our aim is to complete the Shape Calculus by providing verification techniques at specification level.<br />
The objective is to find the right abstractions and boundaries that permit the application of existing<br />
quantitative model checking or quantitative equivalence checking techniques to the evolution of a<br />
given network of Shape Calculus processes. Also suitable logic languages for specifying the properties<br />
must be identified. In such a way we target to improve Shape Calculus to promote a coupling between<br />
the calculus and the BioShape tool to work in synergy towards the gaining of quantitative information<br />
about simulated environments.</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=Poster_Session_at_MLQA_2010&diff=289Poster Session at MLQA 20102010-07-16T13:07:48Z<p>Nataliya: </p>
<hr />
<div>__NOTOC__<br />
We invited posters under two categories:<br />
<br />
* Presentation of recent or on-going work relating to models, logics, tools, and/or applications with respect to discrete, stochastic and/or continuous systems and properties.<br />
<br />
* Overview of the recent research activities of a group, in relation to the themes of MLQA.<br />
<br />
There were 11 poster submissions to the MLQA poster session. Click on a poster title in order to access the correspondent poster submission in the pdf format.<br />
<br />
===Michael Huth, Nir Piterman, Daniel Wagner. [http://wiki.ercim.eu/wg/MLQA/images/1/14/Submission_1.pdf p-Automata Approach to Probabilistic Verification].===<br />
<br />
The poster introduces an automata based approach to the<br />
verification of probabilistic systems. Our so-called<br />
p-automata combine the combinatorial structure of alternating<br />
tree automata with the ability to quantify probabilities of<br />
regular sets of paths. These foundations enable abstraction-based<br />
probabilistic model checking for probabilistic specifications<br />
that subsume Markov chains, PCTL, LTL and CTL* like logics.<br />
<br />
The poster is based on results from "New Foundations for<br />
Discrete-Time Probabilistic Verification" to appear in<br />
Proceedings of QEST 2010.<br />
<br />
=== Nataliya Skrypnyuk, Michael Smith. Abstraction of Stochastic Process Algebras. ===<br />
<br />
Stochastic process algebras are compositional modelling languages<br />
that can be used to describe systems whose behaviour evolves<br />
probabilistically over time - from distributed computer systems, to<br />
signalling pathways in cells. Two such languages are Interactive<br />
Markov Chains (IMC), and the Performance Evaluation Process Algebra<br />
(PEPA), which handle synchronisation between model components in<br />
different ways. The semantics of PEPA can be described as a continuous<br />
time Markov chain (CTMC), whereas for IMC it is a continuous time<br />
Markov decision process (CTMDP).<br />
<br />
In both PEPA and IMC, it is very easy to write a model whose state space<br />
is exponentially larger than its description. It is therefore important to<br />
look for ways to abstract such models, so that they can become small<br />
enough to analyse. Importantly, we want to perform the abstraction at<br />
the language level, so that we maintain the compositionality of the model.<br />
In this poster, we illustrate two different approaches to this - abstraction<br />
of IMC using pathway analysis (a type of static analysis), and abstraction<br />
of PEPA using compositional aggregation of states.<br />
<br />
=== Igor Cappello and Paola Quaglia. Quantitative Assessment of Web Services: Applying SCOWS to a Real-Life Scenario. ===<br />
<br />
We present an example of application of SCOWS to a real-life scenario<br />
(loan request) developed within the SENSORIA European Project. SCOWS<br />
is a stochastic process algebra tailored for the purpose of<br />
quantitative assessment of Web Services: applying the labelled<br />
semantics to a SCOWS service S, it is possible to derive the Labelled<br />
Transition System (LTS) representing all the possible behaviours of S.<br />
The LTS can then be used to generate a CTMC on which quantitative<br />
model checking can take place.<br />
<br />
In order to automatically derive the LTS and minimize the state space<br />
needed to represent it, we implemented SCOWS_lts, a tool written in<br />
Java whose output can be imported in a model checker (e.g. PRISM) and<br />
used to perform quantitative analysis.<br />
<br />
We report some results obtained assessing the impact of one parameter<br />
(the rate at which a clerk processes the submitted loan request) on<br />
the overall performance of the service.<br />
<br />
=== Ender Yüksel, Hanne Riis Nielson, and Flemming Nielson. High Security at a Low Cost. ===<br />
<br />
In the future tiny devices with microcontrollers and sensors will be in charge<br />
of numerous activities in our lives. Tracking our energy consumption and CO2<br />
emission, controlling our living conditions, enforcing security, and monitoring<br />
our health will be some examples of their functions These devices will form<br />
wireless networks to communicate with one another, moreover their power<br />
consumption will be very low. It is not hard to predict that our modern society<br />
will depend on the correct operation of these devices, and the security of the<br />
network they are operating.<br />
<br />
Such sensor-based systems, also known as "cyber-physical systems", achieve<br />
security by means of cryptographic protocols. In a simplistic setting where the<br />
power consumption should be minimum and the processing power is limited, it<br />
is more likely that all devices in the network will share the same cryptographic<br />
key. In this study, we are working on the trade-off between two challenges: <br />
"the cryptographic key should be changed frequently to preserve security" and<br />
"the cryptographic key should be changed rarely to save power". We work on the<br />
ZigBee wireless sensor network standard, that offers the advantages of simple<br />
and low resource communication. We model the system as a continuous-time<br />
Markov chain, and analyze it by posing a number of questions shedding light<br />
on its behaviour. The properties we are interested in are expressed in continuous stochastic logic, and probabilistic model checker Prism is used in the analysis.<br />
<br />
=== Erik de Vink, Suzana Andova, and Luuk Groenewegen. Towards Dynamic Adaptation of Probabilistic Systems. ===<br />
<br />
Dynamic system adaptation is modeled in Paradigm as coordination of<br />
collaborating components. A special component McPal allows for addition<br />
of new behavior, of new constraints and of new control in view of a new<br />
collaboration. McPal gradually adapts the system dynamics. It is shown<br />
that the approach also applies to the probabilistic setting. For a<br />
client-server example, where McPal gradually adds probabilistic behavior<br />
to deterministic components, precise modeling of changing system<br />
dynamics is achieved. This modeling of the transient behavior, spanning<br />
the complete migration range from as-is collaboration to to-be collabo-<br />
ration, serves as a stepping stone for quantitative analysis of the<br />
system during adaptation.<br />
<br />
=== Fuyuan Zhang and Piotr Filipiuk. Model Checking is Static Analysis. ===<br />
<br />
The link between model checking and static analysis has been of great interest<br />
to academia for many years. Early work of Bernhard Steffen and David Schmidt<br />
has shown that classic data-flow analysis is an instance of model checking. The<br />
poster gives an overview of our research aiming to show that also model checking<br />
is static analysis of modal logics and that model checking can be carried by the<br />
static analysis engine; namely ALFP suite. We use Flow Logic, which is a<br />
state-of-the-art approach to static analysis that bridges the gap between a number of approaches to static analysis including Data Flow Analysis, Constraint Based Analysis, Abstract Interpretation and Type and Effect Systems. In the developments it has been demonstrated that Flow Logic is a robust approach that is able to deal with a variety of calculi, programming languages and recently modal logics such as CTL, ACTL and alternation-free mu-calculus. In order to calculate the analysis solution, we use ALFP Suite that computes the least model guaranteed by the Moore family theorem for ALFP. In its current version, the suite supports two solvers, one being a differential worklist solver that is based on a representation of relations as prefix trees and the other being a solver in continuation passing style that is based on a BDD representation of relations.<br />
<br />
=== Vashti Galpin, Jane Hillston, and Luca Bortolussi. A Stochastic Hybrid Process Algebra. ===<br />
<br />
The process algebra HYPE was developed to model hybrid systems which are<br />
those systems that exhibit both discrete and continuous behaviour. Our new<br />
process algebra extends HYPE by including the ability to model stochastic<br />
behaviour.<br />
<br />
The poster will introduce stochastic HYPE, minimising notational overhead and<br />
through the use of a networking example. It will also contain graphs describing<br />
the evolution of the example over time based on stochastic simulation.<br />
<br />
=== David Cachera, Thomas Jensen, Arnaud Jobin, and Pascal Sotin. A Linear Operator Framework for Analysing Resource Usage. ===<br />
<br />
We present a semantics-based framework for analysing the quantitative<br />
behaviour of programs with regard to resource usage. We start from an<br />
operational semantics in which costs are modelled using a dioid<br />
structure, which generalizes the classical (max,plus) semiring<br />
structure over reals. The dioid structure of costs allows for defining<br />
the quantitative semantics as a linear operator. We then develop an<br />
approximation framework of such a semantics in order to effectively<br />
compute global cost information from the program. We show how this<br />
framework is related to, and thus can benefit from, the theory of<br />
abstract interpretation for analyzing qualitative properties, We focus<br />
on the notion of long-run cost which models the asymptotic average<br />
cost of a program, and show that our abstraction technique provides a<br />
correct approximation of the concrete long-run cost. We illustrate our<br />
approach on an application example devoted to the computation of<br />
energy consumption for a language with complex array operations and<br />
explicit energy modes management.<br />
<br />
=== Christoffer Sloth and Rafael Wisniewski. Verification of Continuous Dynamical Systems by Timed Automata. ===<br />
<br />
The poster outlines a method for abstracting continuous dynamical systems by finite<br />
timed automata, which allows automatic verification of continuous systems. The novelty<br />
of the method is that the abstraction is generated from a partition of state space which<br />
is generated by intersecting set-differences of positive invariant sets.<br />
<br />
It is chosen to abstract continuous systems by timed automata, since tools for efficient<br />
verification of such models exist. Additionally, Lyapunov functions are chosen for<br />
generating the partition, because their sub-level sets are positive invariant; hence, it is<br />
possible to determine a priori if the abstraction is sound or complete. Furthermore, for<br />
certain systems it is possible to approximate the reachable set of the continuous system<br />
arbitrarily close by the timed automaton. The structure added to the abstraction by<br />
partitioning the state space by positive invariant sets allows the timed automaton to be<br />
composed of multiple timed automata. This makes it possible to parallelize the verification<br />
process of the timed automaton.<br />
<br />
Some methods require explicit solutions of the differential equations that describe the<br />
continuous dynamics, which are usually unknown. Therefore, the proposed method only<br />
relies on the Lyapunov functions and their derivatives, which can be calculated.<br />
<br />
The proposed abstraction is applied to an example, which illustrates how sound and<br />
complete abstractions are generated.<br />
<br />
=== Lei Song, Flemming Nielson, and Bo Friis Nielson. A Broadcast Based Stochastic Calculus. ===<br />
<br />
In our current work we give a stochastic calculus based on broadcast communication. Only<br />
broadcast actions are associated with rates while all the reception actions are passive and<br />
assigned with weights. By doing so there is no need to handle synchronisation between<br />
actions with different rates. We also give a label transition system of our calculus from<br />
which we can get a CTMC naturally. We show the usefulness of our calculus by giving<br />
several examples from performance analysis setting such as batch Markovian arrival<br />
process (BMAP), marked markovian arrival process (MMAP) and closed queueing networks.<br />
<br />
=== Massimo Callisto De Donato, Flavio Corradini, Maria Rita Di Berardini, Emanuela Merelli, and Luca Tesei. Tailoring the Shape Calculus for Quantitative Analysis. ===<br />
<br />
The Shape Calculus, a bio-inspired language, is a non-deterministic calculus in which processes<br />
are composed of a 3D shape moving in a space and of a behaviour. A process behaviour is formally<br />
expressed as a CCS-like process algebra with deterministic time where channels - the active sites -<br />
are particular surfaces of the shape. A site can bind, after a proper collision, to another compatible<br />
channel forming a more complex shape and a new process. Contextually to the introduction of the<br />
Shape Calculus we defined BioShape, an environment in which a network of Shape Calculus processes,<br />
together with more specific information about motion and behaviour, can be simulated. In particular,<br />
we showed that such a tool is suitable for representing a biological phenomenon at different spatial<br />
and temporal scales and can be used to perform in silico experiments.<br />
<br />
Our aim is to complete the Shape Calculus by providing verification techniques at specification level.<br />
The objective is to find the right abstractions and boundaries that permit the application of existing<br />
quantitative model checking or quantitative equivalence checking techniques to the evolution of a<br />
given network of Shape Calculus processes. Also suitable logic languages for specifying the properties<br />
must be identified. In such a way we target to improve Shape Calculus to promote a coupling between<br />
the calculus and the BioShape tool to work in synergy towards the gaining of quantitative information<br />
about simulated environments.</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=Poster_Session_at_MLQA_2010&diff=288Poster Session at MLQA 20102010-07-16T13:06:44Z<p>Nataliya: </p>
<hr />
<div>__NOTOC__<br />
We invited posters under two categories:<br />
<br />
* Presentation of recent or on-going work relating to models, logics, tools, and/or applications with respect to discrete, stochastic and/or continuous systems and properties.<br />
<br />
* Overview of the recent research activities of a group, in relation to the themes of MLQA.<br />
<br />
There were 11 poster submissions to the MLQA poster session. Click on a poster title in order to access the correspondent poster submission in the pdf format.<br />
<br />
===Michael Huth, Nir Piterman, Daniel Wagner. [http://wiki.ercim.eu/wg/MLQA/index.php/Image:Submission_1.pdf p-Automata Approach to Probabilistic Verification].===<br />
<br />
The poster introduces an automata based approach to the<br />
verification of probabilistic systems. Our so-called<br />
p-automata combine the combinatorial structure of alternating<br />
tree automata with the ability to quantify probabilities of<br />
regular sets of paths. These foundations enable abstraction-based<br />
probabilistic model checking for probabilistic specifications<br />
that subsume Markov chains, PCTL, LTL and CTL* like logics.<br />
<br />
The poster is based on results from "New Foundations for<br />
Discrete-Time Probabilistic Verification" to appear in<br />
Proceedings of QEST 2010.<br />
<br />
=== Nataliya Skrypnyuk, Michael Smith. Abstraction of Stochastic Process Algebras. ===<br />
<br />
Stochastic process algebras are compositional modelling languages<br />
that can be used to describe systems whose behaviour evolves<br />
probabilistically over time - from distributed computer systems, to<br />
signalling pathways in cells. Two such languages are Interactive<br />
Markov Chains (IMC), and the Performance Evaluation Process Algebra<br />
(PEPA), which handle synchronisation between model components in<br />
different ways. The semantics of PEPA can be described as a continuous<br />
time Markov chain (CTMC), whereas for IMC it is a continuous time<br />
Markov decision process (CTMDP).<br />
<br />
In both PEPA and IMC, it is very easy to write a model whose state space<br />
is exponentially larger than its description. It is therefore important to<br />
look for ways to abstract such models, so that they can become small<br />
enough to analyse. Importantly, we want to perform the abstraction at<br />
the language level, so that we maintain the compositionality of the model.<br />
In this poster, we illustrate two different approaches to this - abstraction<br />
of IMC using pathway analysis (a type of static analysis), and abstraction<br />
of PEPA using compositional aggregation of states.<br />
<br />
=== Igor Cappello and Paola Quaglia. Quantitative Assessment of Web Services: Applying SCOWS to a Real-Life Scenario. ===<br />
<br />
We present an example of application of SCOWS to a real-life scenario<br />
(loan request) developed within the SENSORIA European Project. SCOWS<br />
is a stochastic process algebra tailored for the purpose of<br />
quantitative assessment of Web Services: applying the labelled<br />
semantics to a SCOWS service S, it is possible to derive the Labelled<br />
Transition System (LTS) representing all the possible behaviours of S.<br />
The LTS can then be used to generate a CTMC on which quantitative<br />
model checking can take place.<br />
<br />
In order to automatically derive the LTS and minimize the state space<br />
needed to represent it, we implemented SCOWS_lts, a tool written in<br />
Java whose output can be imported in a model checker (e.g. PRISM) and<br />
used to perform quantitative analysis.<br />
<br />
We report some results obtained assessing the impact of one parameter<br />
(the rate at which a clerk processes the submitted loan request) on<br />
the overall performance of the service.<br />
<br />
=== Ender Yüksel, Hanne Riis Nielson, and Flemming Nielson. High Security at a Low Cost. ===<br />
<br />
In the future tiny devices with microcontrollers and sensors will be in charge<br />
of numerous activities in our lives. Tracking our energy consumption and CO2<br />
emission, controlling our living conditions, enforcing security, and monitoring<br />
our health will be some examples of their functions These devices will form<br />
wireless networks to communicate with one another, moreover their power<br />
consumption will be very low. It is not hard to predict that our modern society<br />
will depend on the correct operation of these devices, and the security of the<br />
network they are operating.<br />
<br />
Such sensor-based systems, also known as "cyber-physical systems", achieve<br />
security by means of cryptographic protocols. In a simplistic setting where the<br />
power consumption should be minimum and the processing power is limited, it<br />
is more likely that all devices in the network will share the same cryptographic<br />
key. In this study, we are working on the trade-off between two challenges: <br />
"the cryptographic key should be changed frequently to preserve security" and<br />
"the cryptographic key should be changed rarely to save power". We work on the<br />
ZigBee wireless sensor network standard, that offers the advantages of simple<br />
and low resource communication. We model the system as a continuous-time<br />
Markov chain, and analyze it by posing a number of questions shedding light<br />
on its behaviour. The properties we are interested in are expressed in continuous stochastic logic, and probabilistic model checker Prism is used in the analysis.<br />
<br />
=== Erik de Vink, Suzana Andova, and Luuk Groenewegen. Towards Dynamic Adaptation of Probabilistic Systems. ===<br />
<br />
Dynamic system adaptation is modeled in Paradigm as coordination of<br />
collaborating components. A special component McPal allows for addition<br />
of new behavior, of new constraints and of new control in view of a new<br />
collaboration. McPal gradually adapts the system dynamics. It is shown<br />
that the approach also applies to the probabilistic setting. For a<br />
client-server example, where McPal gradually adds probabilistic behavior<br />
to deterministic components, precise modeling of changing system<br />
dynamics is achieved. This modeling of the transient behavior, spanning<br />
the complete migration range from as-is collaboration to to-be collabo-<br />
ration, serves as a stepping stone for quantitative analysis of the<br />
system during adaptation.<br />
<br />
=== Fuyuan Zhang and Piotr Filipiuk. Model Checking is Static Analysis. ===<br />
<br />
The link between model checking and static analysis has been of great interest<br />
to academia for many years. Early work of Bernhard Steffen and David Schmidt<br />
has shown that classic data-flow analysis is an instance of model checking. The<br />
poster gives an overview of our research aiming to show that also model checking<br />
is static analysis of modal logics and that model checking can be carried by the<br />
static analysis engine; namely ALFP suite. We use Flow Logic, which is a<br />
state-of-the-art approach to static analysis that bridges the gap between a number of approaches to static analysis including Data Flow Analysis, Constraint Based Analysis, Abstract Interpretation and Type and Effect Systems. In the developments it has been demonstrated that Flow Logic is a robust approach that is able to deal with a variety of calculi, programming languages and recently modal logics such as CTL, ACTL and alternation-free mu-calculus. In order to calculate the analysis solution, we use ALFP Suite that computes the least model guaranteed by the Moore family theorem for ALFP. In its current version, the suite supports two solvers, one being a differential worklist solver that is based on a representation of relations as prefix trees and the other being a solver in continuation passing style that is based on a BDD representation of relations.<br />
<br />
=== Vashti Galpin, Jane Hillston, and Luca Bortolussi. A Stochastic Hybrid Process Algebra. ===<br />
<br />
The process algebra HYPE was developed to model hybrid systems which are<br />
those systems that exhibit both discrete and continuous behaviour. Our new<br />
process algebra extends HYPE by including the ability to model stochastic<br />
behaviour.<br />
<br />
The poster will introduce stochastic HYPE, minimising notational overhead and<br />
through the use of a networking example. It will also contain graphs describing<br />
the evolution of the example over time based on stochastic simulation.<br />
<br />
=== David Cachera, Thomas Jensen, Arnaud Jobin, and Pascal Sotin. A Linear Operator Framework for Analysing Resource Usage. ===<br />
<br />
We present a semantics-based framework for analysing the quantitative<br />
behaviour of programs with regard to resource usage. We start from an<br />
operational semantics in which costs are modelled using a dioid<br />
structure, which generalizes the classical (max,plus) semiring<br />
structure over reals. The dioid structure of costs allows for defining<br />
the quantitative semantics as a linear operator. We then develop an<br />
approximation framework of such a semantics in order to effectively<br />
compute global cost information from the program. We show how this<br />
framework is related to, and thus can benefit from, the theory of<br />
abstract interpretation for analyzing qualitative properties, We focus<br />
on the notion of long-run cost which models the asymptotic average<br />
cost of a program, and show that our abstraction technique provides a<br />
correct approximation of the concrete long-run cost. We illustrate our<br />
approach on an application example devoted to the computation of<br />
energy consumption for a language with complex array operations and<br />
explicit energy modes management.<br />
<br />
=== Christoffer Sloth and Rafael Wisniewski. Verification of Continuous Dynamical Systems by Timed Automata. ===<br />
<br />
The poster outlines a method for abstracting continuous dynamical systems by finite<br />
timed automata, which allows automatic verification of continuous systems. The novelty<br />
of the method is that the abstraction is generated from a partition of state space which<br />
is generated by intersecting set-differences of positive invariant sets.<br />
<br />
It is chosen to abstract continuous systems by timed automata, since tools for efficient<br />
verification of such models exist. Additionally, Lyapunov functions are chosen for<br />
generating the partition, because their sub-level sets are positive invariant; hence, it is<br />
possible to determine a priori if the abstraction is sound or complete. Furthermore, for<br />
certain systems it is possible to approximate the reachable set of the continuous system<br />
arbitrarily close by the timed automaton. The structure added to the abstraction by<br />
partitioning the state space by positive invariant sets allows the timed automaton to be<br />
composed of multiple timed automata. This makes it possible to parallelize the verification<br />
process of the timed automaton.<br />
<br />
Some methods require explicit solutions of the differential equations that describe the<br />
continuous dynamics, which are usually unknown. Therefore, the proposed method only<br />
relies on the Lyapunov functions and their derivatives, which can be calculated.<br />
<br />
The proposed abstraction is applied to an example, which illustrates how sound and<br />
complete abstractions are generated.<br />
<br />
=== Lei Song, Flemming Nielson, and Bo Friis Nielson. A Broadcast Based Stochastic Calculus. ===<br />
<br />
In our current work we give a stochastic calculus based on broadcast communication. Only<br />
broadcast actions are associated with rates while all the reception actions are passive and<br />
assigned with weights. By doing so there is no need to handle synchronisation between<br />
actions with different rates. We also give a label transition system of our calculus from<br />
which we can get a CTMC naturally. We show the usefulness of our calculus by giving<br />
several examples from performance analysis setting such as batch Markovian arrival<br />
process (BMAP), marked markovian arrival process (MMAP) and closed queueing networks.<br />
<br />
=== Massimo Callisto De Donato, Flavio Corradini, Maria Rita Di Berardini, Emanuela Merelli, and Luca Tesei. Tailoring the Shape Calculus for Quantitative Analysis. ===<br />
<br />
The Shape Calculus, a bio-inspired language, is a non-deterministic calculus in which processes<br />
are composed of a 3D shape moving in a space and of a behaviour. A process behaviour is formally<br />
expressed as a CCS-like process algebra with deterministic time where channels - the active sites -<br />
are particular surfaces of the shape. A site can bind, after a proper collision, to another compatible<br />
channel forming a more complex shape and a new process. Contextually to the introduction of the<br />
Shape Calculus we defined BioShape, an environment in which a network of Shape Calculus processes,<br />
together with more specific information about motion and behaviour, can be simulated. In particular,<br />
we showed that such a tool is suitable for representing a biological phenomenon at different spatial<br />
and temporal scales and can be used to perform in silico experiments.<br />
<br />
Our aim is to complete the Shape Calculus by providing verification techniques at specification level.<br />
The objective is to find the right abstractions and boundaries that permit the application of existing<br />
quantitative model checking or quantitative equivalence checking techniques to the evolution of a<br />
given network of Shape Calculus processes. Also suitable logic languages for specifying the properties<br />
must be identified. In such a way we target to improve Shape Calculus to promote a coupling between<br />
the calculus and the BioShape tool to work in synergy towards the gaining of quantitative information<br />
about simulated environments.</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=Poster_Session_at_MLQA_2010&diff=287Poster Session at MLQA 20102010-07-16T13:05:09Z<p>Nataliya: </p>
<hr />
<div>__NOTOC__<br />
We invited posters under two categories:<br />
<br />
* Presentation of recent or on-going work relating to models, logics, tools, and/or applications with respect to discrete, stochastic and/or continuous systems and properties.<br />
<br />
* Overview of the recent research activities of a group, in relation to the themes of MLQA.<br />
<br />
There were 11 poster submissions to the MLQA poster session. Click on a poster title in order to access the correspondent poster submission in the pdf format.<br />
<br />
===Michael Huth, Nir Piterman, Daniel Wagner. [p-Automata Approach to Probabilistic Verification].===<br />
<br />
The poster introduces an automata based approach to the<br />
verification of probabilistic systems. Our so-called<br />
p-automata combine the combinatorial structure of alternating<br />
tree automata with the ability to quantify probabilities of<br />
regular sets of paths. These foundations enable abstraction-based<br />
probabilistic model checking for probabilistic specifications<br />
that subsume Markov chains, PCTL, LTL and CTL* like logics.<br />
<br />
The poster is based on results from "New Foundations for<br />
Discrete-Time Probabilistic Verification" to appear in<br />
Proceedings of QEST 2010.<br />
<br />
=== Nataliya Skrypnyuk, Michael Smith. Abstraction of Stochastic Process Algebras. ===<br />
<br />
Stochastic process algebras are compositional modelling languages<br />
that can be used to describe systems whose behaviour evolves<br />
probabilistically over time - from distributed computer systems, to<br />
signalling pathways in cells. Two such languages are Interactive<br />
Markov Chains (IMC), and the Performance Evaluation Process Algebra<br />
(PEPA), which handle synchronisation between model components in<br />
different ways. The semantics of PEPA can be described as a continuous<br />
time Markov chain (CTMC), whereas for IMC it is a continuous time<br />
Markov decision process (CTMDP).<br />
<br />
In both PEPA and IMC, it is very easy to write a model whose state space<br />
is exponentially larger than its description. It is therefore important to<br />
look for ways to abstract such models, so that they can become small<br />
enough to analyse. Importantly, we want to perform the abstraction at<br />
the language level, so that we maintain the compositionality of the model.<br />
In this poster, we illustrate two different approaches to this - abstraction<br />
of IMC using pathway analysis (a type of static analysis), and abstraction<br />
of PEPA using compositional aggregation of states.<br />
<br />
=== Igor Cappello and Paola Quaglia. Quantitative Assessment of Web Services: Applying SCOWS to a Real-Life Scenario. ===<br />
<br />
We present an example of application of SCOWS to a real-life scenario<br />
(loan request) developed within the SENSORIA European Project. SCOWS<br />
is a stochastic process algebra tailored for the purpose of<br />
quantitative assessment of Web Services: applying the labelled<br />
semantics to a SCOWS service S, it is possible to derive the Labelled<br />
Transition System (LTS) representing all the possible behaviours of S.<br />
The LTS can then be used to generate a CTMC on which quantitative<br />
model checking can take place.<br />
<br />
In order to automatically derive the LTS and minimize the state space<br />
needed to represent it, we implemented SCOWS_lts, a tool written in<br />
Java whose output can be imported in a model checker (e.g. PRISM) and<br />
used to perform quantitative analysis.<br />
<br />
We report some results obtained assessing the impact of one parameter<br />
(the rate at which a clerk processes the submitted loan request) on<br />
the overall performance of the service.<br />
<br />
=== Ender Yüksel, Hanne Riis Nielson, and Flemming Nielson. High Security at a Low Cost. ===<br />
<br />
In the future tiny devices with microcontrollers and sensors will be in charge<br />
of numerous activities in our lives. Tracking our energy consumption and CO2<br />
emission, controlling our living conditions, enforcing security, and monitoring<br />
our health will be some examples of their functions These devices will form<br />
wireless networks to communicate with one another, moreover their power<br />
consumption will be very low. It is not hard to predict that our modern society<br />
will depend on the correct operation of these devices, and the security of the<br />
network they are operating.<br />
<br />
Such sensor-based systems, also known as "cyber-physical systems", achieve<br />
security by means of cryptographic protocols. In a simplistic setting where the<br />
power consumption should be minimum and the processing power is limited, it<br />
is more likely that all devices in the network will share the same cryptographic<br />
key. In this study, we are working on the trade-off between two challenges: <br />
"the cryptographic key should be changed frequently to preserve security" and<br />
"the cryptographic key should be changed rarely to save power". We work on the<br />
ZigBee wireless sensor network standard, that offers the advantages of simple<br />
and low resource communication. We model the system as a continuous-time<br />
Markov chain, and analyze it by posing a number of questions shedding light<br />
on its behaviour. The properties we are interested in are expressed in continuous stochastic logic, and probabilistic model checker Prism is used in the analysis.<br />
<br />
=== Erik de Vink, Suzana Andova, and Luuk Groenewegen. Towards Dynamic Adaptation of Probabilistic Systems. ===<br />
<br />
Dynamic system adaptation is modeled in Paradigm as coordination of<br />
collaborating components. A special component McPal allows for addition<br />
of new behavior, of new constraints and of new control in view of a new<br />
collaboration. McPal gradually adapts the system dynamics. It is shown<br />
that the approach also applies to the probabilistic setting. For a<br />
client-server example, where McPal gradually adds probabilistic behavior<br />
to deterministic components, precise modeling of changing system<br />
dynamics is achieved. This modeling of the transient behavior, spanning<br />
the complete migration range from as-is collaboration to to-be collabo-<br />
ration, serves as a stepping stone for quantitative analysis of the<br />
system during adaptation.<br />
<br />
=== Fuyuan Zhang and Piotr Filipiuk. Model Checking is Static Analysis. ===<br />
<br />
The link between model checking and static analysis has been of great interest<br />
to academia for many years. Early work of Bernhard Steffen and David Schmidt<br />
has shown that classic data-flow analysis is an instance of model checking. The<br />
poster gives an overview of our research aiming to show that also model checking<br />
is static analysis of modal logics and that model checking can be carried by the<br />
static analysis engine; namely ALFP suite. We use Flow Logic, which is a<br />
state-of-the-art approach to static analysis that bridges the gap between a number of approaches to static analysis including Data Flow Analysis, Constraint Based Analysis, Abstract Interpretation and Type and Effect Systems. In the developments it has been demonstrated that Flow Logic is a robust approach that is able to deal with a variety of calculi, programming languages and recently modal logics such as CTL, ACTL and alternation-free mu-calculus. In order to calculate the analysis solution, we use ALFP Suite that computes the least model guaranteed by the Moore family theorem for ALFP. In its current version, the suite supports two solvers, one being a differential worklist solver that is based on a representation of relations as prefix trees and the other being a solver in continuation passing style that is based on a BDD representation of relations.<br />
<br />
=== Vashti Galpin, Jane Hillston, and Luca Bortolussi. A Stochastic Hybrid Process Algebra. ===<br />
<br />
The process algebra HYPE was developed to model hybrid systems which are<br />
those systems that exhibit both discrete and continuous behaviour. Our new<br />
process algebra extends HYPE by including the ability to model stochastic<br />
behaviour.<br />
<br />
The poster will introduce stochastic HYPE, minimising notational overhead and<br />
through the use of a networking example. It will also contain graphs describing<br />
the evolution of the example over time based on stochastic simulation.<br />
<br />
=== David Cachera, Thomas Jensen, Arnaud Jobin, and Pascal Sotin. A Linear Operator Framework for Analysing Resource Usage. ===<br />
<br />
We present a semantics-based framework for analysing the quantitative<br />
behaviour of programs with regard to resource usage. We start from an<br />
operational semantics in which costs are modelled using a dioid<br />
structure, which generalizes the classical (max,plus) semiring<br />
structure over reals. The dioid structure of costs allows for defining<br />
the quantitative semantics as a linear operator. We then develop an<br />
approximation framework of such a semantics in order to effectively<br />
compute global cost information from the program. We show how this<br />
framework is related to, and thus can benefit from, the theory of<br />
abstract interpretation for analyzing qualitative properties, We focus<br />
on the notion of long-run cost which models the asymptotic average<br />
cost of a program, and show that our abstraction technique provides a<br />
correct approximation of the concrete long-run cost. We illustrate our<br />
approach on an application example devoted to the computation of<br />
energy consumption for a language with complex array operations and<br />
explicit energy modes management.<br />
<br />
=== Christoffer Sloth and Rafael Wisniewski. Verification of Continuous Dynamical Systems by Timed Automata. ===<br />
<br />
The poster outlines a method for abstracting continuous dynamical systems by finite<br />
timed automata, which allows automatic verification of continuous systems. The novelty<br />
of the method is that the abstraction is generated from a partition of state space which<br />
is generated by intersecting set-differences of positive invariant sets.<br />
<br />
It is chosen to abstract continuous systems by timed automata, since tools for efficient<br />
verification of such models exist. Additionally, Lyapunov functions are chosen for<br />
generating the partition, because their sub-level sets are positive invariant; hence, it is<br />
possible to determine a priori if the abstraction is sound or complete. Furthermore, for<br />
certain systems it is possible to approximate the reachable set of the continuous system<br />
arbitrarily close by the timed automaton. The structure added to the abstraction by<br />
partitioning the state space by positive invariant sets allows the timed automaton to be<br />
composed of multiple timed automata. This makes it possible to parallelize the verification<br />
process of the timed automaton.<br />
<br />
Some methods require explicit solutions of the differential equations that describe the<br />
continuous dynamics, which are usually unknown. Therefore, the proposed method only<br />
relies on the Lyapunov functions and their derivatives, which can be calculated.<br />
<br />
The proposed abstraction is applied to an example, which illustrates how sound and<br />
complete abstractions are generated.<br />
<br />
=== Lei Song, Flemming Nielson, and Bo Friis Nielson. A Broadcast Based Stochastic Calculus. ===<br />
<br />
In our current work we give a stochastic calculus based on broadcast communication. Only<br />
broadcast actions are associated with rates while all the reception actions are passive and<br />
assigned with weights. By doing so there is no need to handle synchronisation between<br />
actions with different rates. We also give a label transition system of our calculus from<br />
which we can get a CTMC naturally. We show the usefulness of our calculus by giving<br />
several examples from performance analysis setting such as batch Markovian arrival<br />
process (BMAP), marked markovian arrival process (MMAP) and closed queueing networks.<br />
<br />
=== Massimo Callisto De Donato, Flavio Corradini, Maria Rita Di Berardini, Emanuela Merelli, and Luca Tesei. Tailoring the Shape Calculus for Quantitative Analysis. ===<br />
<br />
The Shape Calculus, a bio-inspired language, is a non-deterministic calculus in which processes<br />
are composed of a 3D shape moving in a space and of a behaviour. A process behaviour is formally<br />
expressed as a CCS-like process algebra with deterministic time where channels - the active sites -<br />
are particular surfaces of the shape. A site can bind, after a proper collision, to another compatible<br />
channel forming a more complex shape and a new process. Contextually to the introduction of the<br />
Shape Calculus we defined BioShape, an environment in which a network of Shape Calculus processes,<br />
together with more specific information about motion and behaviour, can be simulated. In particular,<br />
we showed that such a tool is suitable for representing a biological phenomenon at different spatial<br />
and temporal scales and can be used to perform in silico experiments.<br />
<br />
Our aim is to complete the Shape Calculus by providing verification techniques at specification level.<br />
The objective is to find the right abstractions and boundaries that permit the application of existing<br />
quantitative model checking or quantitative equivalence checking techniques to the evolution of a<br />
given network of Shape Calculus processes. Also suitable logic languages for specifying the properties<br />
must be identified. In such a way we target to improve Shape Calculus to promote a coupling between<br />
the calculus and the BioShape tool to work in synergy towards the gaining of quantitative information<br />
about simulated environments.</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=Poster_Session_at_MLQA_2010&diff=286Poster Session at MLQA 20102010-07-16T13:02:53Z<p>Nataliya: </p>
<hr />
<div>__NOTOC__<br />
We invited posters under two categories:<br />
<br />
* Presentation of recent or on-going work relating to models, logics, tools, and/or applications with respect to discrete, stochastic and/or continuous systems and properties.<br />
<br />
* Overview of the recent research activities of a group, in relation to the themes of MLQA.<br />
<br />
There were 11 poster submissions to the MLQA poster session. Click on a poster title in order to access the correspondent poster submission in the pdf format.<br />
<br />
===Michael Huth, Nir Piterman, Daniel Wagner. [p-Automata Approach to Probabilistic Verification].===<br />
<br />
The poster introduces an automata based approach to the<br />
verification of probabilistic systems. Our so-called<br />
p-automata combine the combinatorial structure of alternating<br />
tree automata with the ability to quantify probabilities of<br />
regular sets of paths. These foundations enable abstraction-based<br />
probabilistic model checking for probabilistic specifications<br />
that subsume Markov chains, PCTL, LTL and CTL* like logics.<br />
<br />
The poster is based on results from "New Foundations for<br />
Discrete-Time Probabilistic Verification" to appear in<br />
Proceedings of QEST 2010.<br />
<br />
=== Nataliya Skrypnyuk, Michael Smith. Abstraction of Stochastic Process Algebras. ===<br />
<br />
Stochastic process algebras are compositional modelling languages<br />
that can be used to describe systems whose behaviour evolves<br />
probabilistically over time - from distributed computer systems, to<br />
signalling pathways in cells. Two such languages are Interactive<br />
Markov Chains (IMC), and the Performance Evaluation Process Algebra<br />
(PEPA), which handle synchronisation between model components in<br />
different ways. The semantics of PEPA can be described as a continuous<br />
time Markov chain (CTMC), whereas for IMC it is a continuous time<br />
Markov decision process (CTMDP).<br />
<br />
In both PEPA and IMC, it is very easy to write a model whose state space<br />
is exponentially larger than its description. It is therefore important to<br />
look for ways to abstract such models, so that they can become small<br />
enough to analyse. Importantly, we want to perform the abstraction at<br />
the language level, so that we maintain the compositionality of the model.<br />
In this poster, we illustrate two different approaches to this - abstraction<br />
of IMC using pathway analysis (a type of static analysis), and abstraction<br />
of PEPA using compositional aggregation of states.<br />
<br />
=== Igor Cappello and Paola Quaglia. Quantitative Assessment of Web Services: Applying SCOWS to a Real-Life Scenario. ===<br />
<br />
We present an example of application of SCOWS to a real-life scenario<br />
(loan request) developed within the SENSORIA European Project. SCOWS<br />
is a stochastic process algebra tailored for the purpose of<br />
quantitative assessment of Web Services: applying the labelled<br />
semantics to a SCOWS service S, it is possible to derive the Labelled<br />
Transition System (LTS) representing all the possible behaviours of S.<br />
The LTS can then be used to generate a CTMC on which quantitative<br />
model checking can take place.<br />
<br />
In order to automatically derive the LTS and minimize the state space<br />
needed to represent it, we implemented SCOWS_lts, a tool written in<br />
Java whose output can be imported in a model checker (e.g. PRISM) and<br />
used to perform quantitative analysis.<br />
<br />
We report some results obtained assessing the impact of one parameter<br />
(the rate at which a clerk processes the submitted loan request) on<br />
the overall performance of the service.<br />
<br />
=== Ender Yüksel, Hanne Riis Nielson, and Flemming Nielson. High Security at a Low Cost. ===<br />
<br />
In the future tiny devices with microcontrollers and sensors will be in charge<br />
of numerous activities in our lives. Tracking our energy consumption and CO2<br />
emission, controlling our living conditions, enforcing security, and monitoring<br />
our health will be some examples of their functions These devices will form<br />
wireless networks to communicate with one another, moreover their power<br />
consumption will be very low. It is not hard to predict that our modern society<br />
will depend on the correct operation of these devices, and the security of the<br />
network they are operating.<br />
<br />
Such sensor-based systems, also known as "cyber-physical systems", achieve<br />
security by means of cryptographic protocols. In a simplistic setting where the<br />
power consumption should be minimum and the processing power is limited, it<br />
is more likely that all devices in the network will share the same cryptographic<br />
key. In this study, we are working on the trade-off between two challenges: <br />
"the cryptographic key should be changed frequently to preserve security" and<br />
"the cryptographic key should be changed rarely to save power". We work on the<br />
ZigBee wireless sensor network standard, that offers the advantages of simple<br />
and low resource communication. We model the system as a continuous-time<br />
Markov chain, and analyze it by posing a number of questions shedding light<br />
on its behaviour. The properties we are interested in are expressed in continuous stochastic logic, and probabilistic model checker Prism is used in the analysis.<br />
<br />
=== Erik de Vink, Suzana Andova, and Luuk Groenewegen. Towards Dynamic Adaptation of Probabilistic Systems. ===<br />
<br />
Dynamic system adaptation is modeled in Paradigm as coordination of<br />
collaborating components. A special component McPal allows for addition<br />
of new behavior, of new constraints and of new control in view of a new<br />
collaboration. McPal gradually adapts the system dynamics. It is shown<br />
that the approach also applies to the probabilistic setting. For a<br />
client-server example, where McPal gradually adds probabilistic behavior<br />
to deterministic components, precise modeling of changing system<br />
dynamics is achieved. This modeling of the transient behavior, spanning<br />
the complete migration range from as-is collaboration to to-be collabo-<br />
ration, serves as a stepping stone for quantitative analysis of the<br />
system during adaptation.<br />
<br />
=== Fuyuan Zhang and Piotr Filipiuk. Model Checking is Static Analysis. ===<br />
<br />
The link between model checking and static analysis has been of great interest<br />
to academia for many years. Early work of Bernhard Steffen and David Schmidt<br />
has shown that classic data-flow analysis is an instance of model checking. The<br />
poster gives an overview of our research aiming to show that also model checking<br />
is static analysis of modal logics and that model checking can be carried by the<br />
static analysis engine; namely ALFP suite. We use Flow Logic, which is a<br />
state-of-the-art approach to static analysis that bridges the gap between a number of approaches to static analysis including Data Flow Analysis, Constraint Based Analysis, Abstract Interpretation and Type and Effect Systems. In the developments it has been demonstrated that Flow Logic is a robust approach that is able to deal with a variety of calculi, programming languages and recently modal logics such as CTL, ACTL and alternation-free mu-calculus. In order to calculate the analysis solution, we use ALFP Suite that computes the least model guaranteed by the Moore family theorem for ALFP. In its current version, the suite supports two solvers, one being a differential worklist solver that is based on a representation of relations as prefix trees and the other being a solver in continuation passing style that is based on a BDD representation of relations.<br />
<br />
=== Vashti Galpin, Jane Hillston, and Luca Bortolussi. A Stochastic Hybrid Process Algebra. ===<br />
<br />
The process algebra HYPE was developed to model hybrid systems which are<br />
those systems that exhibit both discrete and continuous behaviour. Our new<br />
process algebra extends HYPE by including the ability to model stochastic<br />
behaviour.<br />
<br />
The poster will introduce stochastic HYPE, minimising notational overhead and<br />
through the use of a networking example. It will also contain graphs describing<br />
the evolution of the example over time based on stochastic simulation.<br />
===<br />
<br />
=== Submission 8 ===<br />
Corresponding Author: Arnaud Jobin <arnaud.jobin@irisa.fr><br />
Title: A Linear Operator Framework for Analysing Resource Usage<br />
Authors: David Cachera, Thomas Jensen, Arnaud Jobin, and Pascal Sotin<br />
<br />
We present a semantics-based framework for analysing the quantitative<br />
behaviour of programs with regard to resource usage. We start from an<br />
operational semantics in which costs are modelled using a dioid<br />
structure, which generalizes the classical (max,plus) semiring<br />
structure over reals. The dioid structure of costs allows for defining<br />
the quantitative semantics as a linear operator. We then develop an<br />
approximation framework of such a semantics in order to effectively<br />
compute global cost information from the program. We show how this<br />
framework is related to, and thus can benefit from, the theory of<br />
abstract interpretation for analyzing qualitative properties, We focus<br />
on the notion of long-run cost which models the asymptotic average<br />
cost of a program, and show that our abstraction technique provides a<br />
correct approximation of the concrete long-run cost. We illustrate our<br />
approach on an application example devoted to the computation of<br />
energy consumption for a language with complex array operations and<br />
explicit energy modes management.<br />
===<br />
<br />
=== Submission 9 ===<br />
Corresponding Author: Christoffer Sloth <csloth@cs.aau.dk><br />
Title: Verification of Continuous Dynamical Systems by Timed Automata<br />
Authors: Christoffer Sloth and Rafael Wisniewski<br />
<br />
The poster outlines a method for abstracting continuous dynamical systems by finite<br />
timed automata, which allows automatic verification of continuous systems. The novelty<br />
of the method is that the abstraction is generated from a partition of state space which<br />
is generated by intersecting set-differences of positive invariant sets.<br />
<br />
It is chosen to abstract continuous systems by timed automata, since tools for efficient<br />
verification of such models exist. Additionally, Lyapunov functions are chosen for<br />
generating the partition, because their sub-level sets are positive invariant; hence, it is<br />
possible to determine a priori if the abstraction is sound or complete. Furthermore, for<br />
certain systems it is possible to approximate the reachable set of the continuous system<br />
arbitrarily close by the timed automaton. The structure added to the abstraction by<br />
partitioning the state space by positive invariant sets allows the timed automaton to be<br />
composed of multiple timed automata. This makes it possible to parallelize the verification<br />
process of the timed automaton.<br />
<br />
Some methods require explicit solutions of the differential equations that describe the<br />
continuous dynamics, which are usually unknown. Therefore, the proposed method only<br />
relies on the Lyapunov functions and their derivatives, which can be calculated.<br />
<br />
The proposed abstraction is applied to an example, which illustrates how sound and<br />
complete abstractions are generated.<br />
===<br />
<br />
=== Submission 10 ===<br />
Corresponding Author: Lei Song <leis@itu.dk><br />
Title: A Broadcast Based Stochastic Calculus<br />
Authors: Lei Song, Flemming Nielson, and Bo Friis Nielson<br />
<br />
In our current work we give a stochastic calculus based on broadcast communication. Only<br />
broadcast actions are associated with rates while all the reception actions are passive and<br />
assigned with weights. By doing so there is no need to handle synchronisation between<br />
actions with different rates. We also give a label transition system of our calculus from<br />
which we can get a CTMC naturally. We show the usefulness of our calculus by giving<br />
several examples from performance analysis setting such as batch Markovian arrival<br />
process (BMAP), marked markovian arrival process (MMAP) and closed queueing networks.<br />
===<br />
<br />
=== Submission 11 ===<br />
Corresponding Author: Massimo Callisto <massimo.callisto@unicam.it><br />
Title: Tailoring the Shape Calculus for Quantitative Analysis<br />
Authors: Massimo Callisto De Donato, Flavio Corradini, Maria Rita Di Berardini, Emanuela Merelli, and Luca Tesei<br />
<br />
The Shape Calculus, a bio-inspired language, is a non-deterministic calculus in which processes<br />
are composed of a 3D shape moving in a space and of a behaviour. A process behaviour is formally<br />
expressed as a CCS-like process algebra with deterministic time where channels - the active sites -<br />
are particular surfaces of the shape. A site can bind, after a proper collision, to another compatible<br />
channel forming a more complex shape and a new process. Contextually to the introduction of the<br />
Shape Calculus we defined BioShape, an environment in which a network of Shape Calculus processes,<br />
together with more specific information about motion and behaviour, can be simulated. In particular,<br />
we showed that such a tool is suitable for representing a biological phenomenon at different spatial<br />
and temporal scales and can be used to perform in silico experiments.<br />
<br />
Our aim is to complete the Shape Calculus by providing verification techniques at specification level.<br />
The objective is to find the right abstractions and boundaries that permit the application of existing<br />
quantitative model checking or quantitative equivalence checking techniques to the evolution of a<br />
given network of Shape Calculus processes. Also suitable logic languages for specifying the properties<br />
must be identified. In such a way we target to improve Shape Calculus to promote a coupling between<br />
the calculus and the BioShape tool to work in synergy towards the gaining of quantitative information<br />
about simulated environments.<br />
===</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=Poster_Session_at_MLQA_2010&diff=285Poster Session at MLQA 20102010-07-16T12:53:32Z<p>Nataliya: </p>
<hr />
<div>__NOTOC__<br />
We invited posters under two categories:<br />
<br />
* Presentation of recent or on-going work relating to models, logics, tools, and/or applications with respect to discrete, stochastic and/or continuous systems and properties.<br />
<br />
* Overview of the recent research activities of a group, in relation to the themes of MLQA.<br />
<br />
There were 11 poster submissions to the MLQA poster session. Click on a poster title in order to access the correspondent poster submission in the pdf format.<br />
<br />
===Michael Huth, Nir Piterman, Daniel Wagner. [p-Automata Approach to Probabilistic Verification].===<br />
<br />
The poster introduces an automata based approach to the<br />
verification of probabilistic systems. Our so-called<br />
p-automata combine the combinatorial structure of alternating<br />
tree automata with the ability to quantify probabilities of<br />
regular sets of paths. These foundations enable abstraction-based<br />
probabilistic model checking for probabilistic specifications<br />
that subsume Markov chains, PCTL, LTL and CTL* like logics.<br />
<br />
The poster is based on results from "New Foundations for<br />
Discrete-Time Probabilistic Verification" to appear in<br />
Proceedings of QEST 2010.<br />
<br />
=== Submission 2 ===<br />
Corresponding Author: N/A<br />
Title: Abstraction of Stochastic Process Algebras<br />
Authors: Nataliya Skrypnyuk, Michael Smith<br />
<br />
Stochastic process algebras are compositional modelling languages<br />
that can be used to describe systems whose behaviour evolves<br />
probabilistically over time - from distributed computer systems, to<br />
signalling pathways in cells. Two such languages are Interactive<br />
Markov Chains (IMC), and the Performance Evaluation Process Algebra<br />
(PEPA), which handle synchronisation between model components in<br />
different ways. The semantics of PEPA can be described as a continuous<br />
time Markov chain (CTMC), whereas for IMC it is a continuous time<br />
Markov decision process (CTMDP).<br />
<br />
In both PEPA and IMC, it is very easy to write a model whose state space<br />
is exponentially larger than its description. It is therefore important to<br />
look for ways to abstract such models, so that they can become small<br />
enough to analyse. Importantly, we want to perform the abstraction at<br />
the language level, so that we maintain the compositionality of the model.<br />
In this poster, we illustrate two different approaches to this - abstraction<br />
of IMC using pathway analysis (a type of static analysis), and abstraction<br />
of PEPA using compositional aggregation of states.<br />
===<br />
<br />
=== Submission 3 ===<br />
Corresponding Author: Igor Cappello <cappello@disi.unitn.it><br />
Title: Quantitative Assessment of Web Services: Applying SCOWS to a Real-Life Scenario<br />
Authors: Igor Cappello and Paola Quaglia<br />
<br />
We present an example of application of SCOWS to a real-life scenario<br />
(loan request) developed within the SENSORIA European Project. SCOWS<br />
is a stochastic process algebra tailored for the purpose of<br />
quantitative assessment of Web Services: applying the labelled<br />
semantics to a SCOWS service S, it is possible to derive the Labelled<br />
Transition System (LTS) representing all the possible behaviours of S.<br />
The LTS can then be used to generate a CTMC on which quantitative<br />
model checking can take place.<br />
<br />
In order to automatically derive the LTS and minimize the state space<br />
needed to represent it, we implemented SCOWS_lts, a tool written in<br />
Java whose output can be imported in a model checker (e.g. PRISM) and<br />
used to perform quantitative analysis.<br />
<br />
We report some results obtained assessing the impact of one parameter<br />
(the rate at which a clerk processes the submitted loan request) on<br />
the overall performance of the service.<br />
===<br />
<br />
=== Submission 4 ===<br />
Corresponding Author: Ender Yüksel <ey@imm.dtu.dk><br />
Title: High Security at a Low Cost<br />
Authors: Ender Yüksel, Hanne Riis Nielson, and Flemming Nielson<br />
<br />
In the future tiny devices with microcontrollers and sensors will be in charge<br />
of numerous activities in our lives. Tracking our energy consumption and CO2<br />
emission, controlling our living conditions, enforcing security, and monitoring<br />
our health will be some examples of their functions These devices will form<br />
wireless networks to communicate with one another, moreover their power<br />
consumption will be very low. It is not hard to predict that our modern society<br />
will depend on the correct operation of these devices, and the security of the<br />
network they are operating.<br />
<br />
Such sensor-based systems, also known as "cyber-physical systems", achieve<br />
security by means of cryptographic protocols. In a simplistic setting where the<br />
power consumption should be minimum and the processing power is limited, it<br />
is more likely that all devices in the network will share the same cryptographic<br />
key. In this study, we are working on the trade-off between two challenges: <br />
"the cryptographic key should be changed frequently to preserve security" and<br />
"the cryptographic key should be changed rarely to save power". We work on the<br />
ZigBee wireless sensor network standard, that offers the advantages of simple<br />
and low resource communication. We model the system as a continuous-time<br />
Markov chain, and analyze it by posing a number of questions shedding light<br />
on its behaviour. The properties we are interested in are expressed in continuous<br />
stochastic logic, and probabilistic model checker Prism is used in the analysis.<br />
===<br />
<br />
=== Submission 5 ===<br />
Corresponding Author: Erik de Vink <evink@win.tue.nl><br />
Title: Towards Dynamic Adaptation of Probabilistic Systems<br />
Authors: Erik de Vink, Suzana Andova, and Luuk Groenewegen<br />
<br />
Dynamic system adaptation is modeled in Paradigm as coordination of<br />
collaborating components. A special component McPal allows for addition<br />
of new behavior, of new constraints and of new control in view of a new<br />
collaboration. McPal gradually adapts the system dynamics. It is shown<br />
that the approach also applies to the probabilistic setting. For a<br />
client-server example, where McPal gradually adds probabilistic behavior<br />
to deterministic components, precise modeling of changing system<br />
dynamics is achieved. This modeling of the transient behavior, spanning<br />
the complete migration range from as-is collaboration to to-be collabo-<br />
ration, serves as a stepping stone for quantitative analysis of the<br />
system during adaptation.<br />
===<br />
<br />
=== Submission 6 ===<br />
Corresponding Author: Fuyuan Zhang <fuzh@imm.dtu.dk><br />
Title: Model Checking is Static Analysis<br />
Authors: Fuyuan Zhang and Piotr Filipiuk<br />
<br />
The link between model checking and static analysis has been of great interest<br />
to academia for many years. Early work of Bernhard Steffen and David Schmidt<br />
has shown that classic data-flow analysis is an instance of model checking. The<br />
poster gives an overview of our research aiming to show that also model checking<br />
is static analysis of modal logics and that model checking can be carried by the<br />
static analysis engine; namely ALFP suite. We use Flow Logic, which is a<br />
state-of-the-art approach to static analysis that bridges the gap between a number<br />
of approaches to static analysis including Data Flow Analysis, Constraint Based<br />
Analysis, Abstract Interpretation and Type and Effect Systems. In the developments<br />
it has been demonstrated that Flow Logic is a robust approach that is able to deal<br />
with a variety of calculi, programming languages and recently modal logics such as<br />
CTL, ACTL and alternation-free mu-calculus. In order to calculate the analysis<br />
solution, we use ALFP Suite that computes the least model guaranteed by the Moore<br />
family theorem for ALFP. In its current version, the suite supports two solvers, one<br />
being a differential worklist solver that is based on a representation of relations as<br />
prefix trees and the other being a solver in continuation passing style that is based<br />
on a BDD representation of relations.<br />
===<br />
<br />
=== Submission 7 ===<br />
Corresponding Author: Vashti Galpin <Vashti.Galpin@ed.ac.uk><br />
Title: A Stochastic Hybrid Process Algebra<br />
Authors: Vashti Galpin, Jane Hillston, and Luca Bortolussi<br />
<br />
The process algebra HYPE was developed to model hybrid systems which are<br />
those systems that exhibit both discrete and continuous behaviour. Our new<br />
process algebra extends HYPE by including the ability to model stochastic<br />
behaviour.<br />
<br />
The poster will introduce stochastic HYPE, minimising notational overhead and<br />
through the use of a networking example. It will also contain graphs describing<br />
the evolution of the example over time based on stochastic simulation.<br />
===<br />
<br />
=== Submission 8 ===<br />
Corresponding Author: Arnaud Jobin <arnaud.jobin@irisa.fr><br />
Title: A Linear Operator Framework for Analysing Resource Usage<br />
Authors: David Cachera, Thomas Jensen, Arnaud Jobin, and Pascal Sotin<br />
<br />
We present a semantics-based framework for analysing the quantitative<br />
behaviour of programs with regard to resource usage. We start from an<br />
operational semantics in which costs are modelled using a dioid<br />
structure, which generalizes the classical (max,plus) semiring<br />
structure over reals. The dioid structure of costs allows for defining<br />
the quantitative semantics as a linear operator. We then develop an<br />
approximation framework of such a semantics in order to effectively<br />
compute global cost information from the program. We show how this<br />
framework is related to, and thus can benefit from, the theory of<br />
abstract interpretation for analyzing qualitative properties, We focus<br />
on the notion of long-run cost which models the asymptotic average<br />
cost of a program, and show that our abstraction technique provides a<br />
correct approximation of the concrete long-run cost. We illustrate our<br />
approach on an application example devoted to the computation of<br />
energy consumption for a language with complex array operations and<br />
explicit energy modes management.<br />
===<br />
<br />
=== Submission 9 ===<br />
Corresponding Author: Christoffer Sloth <csloth@cs.aau.dk><br />
Title: Verification of Continuous Dynamical Systems by Timed Automata<br />
Authors: Christoffer Sloth and Rafael Wisniewski<br />
<br />
The poster outlines a method for abstracting continuous dynamical systems by finite<br />
timed automata, which allows automatic verification of continuous systems. The novelty<br />
of the method is that the abstraction is generated from a partition of state space which<br />
is generated by intersecting set-differences of positive invariant sets.<br />
<br />
It is chosen to abstract continuous systems by timed automata, since tools for efficient<br />
verification of such models exist. Additionally, Lyapunov functions are chosen for<br />
generating the partition, because their sub-level sets are positive invariant; hence, it is<br />
possible to determine a priori if the abstraction is sound or complete. Furthermore, for<br />
certain systems it is possible to approximate the reachable set of the continuous system<br />
arbitrarily close by the timed automaton. The structure added to the abstraction by<br />
partitioning the state space by positive invariant sets allows the timed automaton to be<br />
composed of multiple timed automata. This makes it possible to parallelize the verification<br />
process of the timed automaton.<br />
<br />
Some methods require explicit solutions of the differential equations that describe the<br />
continuous dynamics, which are usually unknown. Therefore, the proposed method only<br />
relies on the Lyapunov functions and their derivatives, which can be calculated.<br />
<br />
The proposed abstraction is applied to an example, which illustrates how sound and<br />
complete abstractions are generated.<br />
===<br />
<br />
=== Submission 10 ===<br />
Corresponding Author: Lei Song <leis@itu.dk><br />
Title: A Broadcast Based Stochastic Calculus<br />
Authors: Lei Song, Flemming Nielson, and Bo Friis Nielson<br />
<br />
In our current work we give a stochastic calculus based on broadcast communication. Only<br />
broadcast actions are associated with rates while all the reception actions are passive and<br />
assigned with weights. By doing so there is no need to handle synchronisation between<br />
actions with different rates. We also give a label transition system of our calculus from<br />
which we can get a CTMC naturally. We show the usefulness of our calculus by giving<br />
several examples from performance analysis setting such as batch Markovian arrival<br />
process (BMAP), marked markovian arrival process (MMAP) and closed queueing networks.<br />
===<br />
<br />
=== Submission 11 ===<br />
Corresponding Author: Massimo Callisto <massimo.callisto@unicam.it><br />
Title: Tailoring the Shape Calculus for Quantitative Analysis<br />
Authors: Massimo Callisto De Donato, Flavio Corradini, Maria Rita Di Berardini, Emanuela Merelli, and Luca Tesei<br />
<br />
The Shape Calculus, a bio-inspired language, is a non-deterministic calculus in which processes<br />
are composed of a 3D shape moving in a space and of a behaviour. A process behaviour is formally<br />
expressed as a CCS-like process algebra with deterministic time where channels - the active sites -<br />
are particular surfaces of the shape. A site can bind, after a proper collision, to another compatible<br />
channel forming a more complex shape and a new process. Contextually to the introduction of the<br />
Shape Calculus we defined BioShape, an environment in which a network of Shape Calculus processes,<br />
together with more specific information about motion and behaviour, can be simulated. In particular,<br />
we showed that such a tool is suitable for representing a biological phenomenon at different spatial<br />
and temporal scales and can be used to perform in silico experiments.<br />
<br />
Our aim is to complete the Shape Calculus by providing verification techniques at specification level.<br />
The objective is to find the right abstractions and boundaries that permit the application of existing<br />
quantitative model checking or quantitative equivalence checking techniques to the evolution of a<br />
given network of Shape Calculus processes. Also suitable logic languages for specifying the properties<br />
must be identified. In such a way we target to improve Shape Calculus to promote a coupling between<br />
the calculus and the BioShape tool to work in synergy towards the gaining of quantitative information<br />
about simulated environments.<br />
===</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=Poster_Session_at_MLQA_2010&diff=284Poster Session at MLQA 20102010-07-16T12:53:11Z<p>Nataliya: </p>
<hr />
<div>__NOTOC__<br />
We invited posters under two categories:<br />
<br />
* Presentation of recent or on-going work relating to models, logics, tools, and/or applications with respect to discrete, stochastic and/or continuous systems and properties.<br />
<br />
* Overview of the recent research activities of a group, in relation to the themes of MLQA.<br />
<br />
There were 11 poster submissions to the MLQA poster session. Click on a poster title in order to access the correspondent poster submission in the pdf format.<br />
<br />
===Michael Huth, Nir Piterman, Daniel Wagner. [p-Automata Approach to Probabilistic Verification].===<br />
<br />
The poster introduces an automata based approach to the<br />
verification of probabilistic systems. Our so-called<br />
p-automata combine the combinatorial structure of alternating<br />
tree automata with the ability to quantify probabilities of<br />
regular sets of paths. These foundations enable abstraction-based<br />
probabilistic model checking for probabilistic specifications<br />
that subsume Markov chains, PCTL, LTL and CTL* like logics.<br />
<br />
The poster is based on results from "New Foundations for<br />
Discrete-Time Probabilistic Verification" to appear in<br />
Proceedings of QEST 2010.<br />
===<br />
<br />
=== Submission 2 ===<br />
Corresponding Author: N/A<br />
Title: Abstraction of Stochastic Process Algebras<br />
Authors: Nataliya Skrypnyuk, Michael Smith<br />
<br />
Stochastic process algebras are compositional modelling languages<br />
that can be used to describe systems whose behaviour evolves<br />
probabilistically over time - from distributed computer systems, to<br />
signalling pathways in cells. Two such languages are Interactive<br />
Markov Chains (IMC), and the Performance Evaluation Process Algebra<br />
(PEPA), which handle synchronisation between model components in<br />
different ways. The semantics of PEPA can be described as a continuous<br />
time Markov chain (CTMC), whereas for IMC it is a continuous time<br />
Markov decision process (CTMDP).<br />
<br />
In both PEPA and IMC, it is very easy to write a model whose state space<br />
is exponentially larger than its description. It is therefore important to<br />
look for ways to abstract such models, so that they can become small<br />
enough to analyse. Importantly, we want to perform the abstraction at<br />
the language level, so that we maintain the compositionality of the model.<br />
In this poster, we illustrate two different approaches to this - abstraction<br />
of IMC using pathway analysis (a type of static analysis), and abstraction<br />
of PEPA using compositional aggregation of states.<br />
===<br />
<br />
=== Submission 3 ===<br />
Corresponding Author: Igor Cappello <cappello@disi.unitn.it><br />
Title: Quantitative Assessment of Web Services: Applying SCOWS to a Real-Life Scenario<br />
Authors: Igor Cappello and Paola Quaglia<br />
<br />
We present an example of application of SCOWS to a real-life scenario<br />
(loan request) developed within the SENSORIA European Project. SCOWS<br />
is a stochastic process algebra tailored for the purpose of<br />
quantitative assessment of Web Services: applying the labelled<br />
semantics to a SCOWS service S, it is possible to derive the Labelled<br />
Transition System (LTS) representing all the possible behaviours of S.<br />
The LTS can then be used to generate a CTMC on which quantitative<br />
model checking can take place.<br />
<br />
In order to automatically derive the LTS and minimize the state space<br />
needed to represent it, we implemented SCOWS_lts, a tool written in<br />
Java whose output can be imported in a model checker (e.g. PRISM) and<br />
used to perform quantitative analysis.<br />
<br />
We report some results obtained assessing the impact of one parameter<br />
(the rate at which a clerk processes the submitted loan request) on<br />
the overall performance of the service.<br />
===<br />
<br />
=== Submission 4 ===<br />
Corresponding Author: Ender Yüksel <ey@imm.dtu.dk><br />
Title: High Security at a Low Cost<br />
Authors: Ender Yüksel, Hanne Riis Nielson, and Flemming Nielson<br />
<br />
In the future tiny devices with microcontrollers and sensors will be in charge<br />
of numerous activities in our lives. Tracking our energy consumption and CO2<br />
emission, controlling our living conditions, enforcing security, and monitoring<br />
our health will be some examples of their functions These devices will form<br />
wireless networks to communicate with one another, moreover their power<br />
consumption will be very low. It is not hard to predict that our modern society<br />
will depend on the correct operation of these devices, and the security of the<br />
network they are operating.<br />
<br />
Such sensor-based systems, also known as "cyber-physical systems", achieve<br />
security by means of cryptographic protocols. In a simplistic setting where the<br />
power consumption should be minimum and the processing power is limited, it<br />
is more likely that all devices in the network will share the same cryptographic<br />
key. In this study, we are working on the trade-off between two challenges: <br />
"the cryptographic key should be changed frequently to preserve security" and<br />
"the cryptographic key should be changed rarely to save power". We work on the<br />
ZigBee wireless sensor network standard, that offers the advantages of simple<br />
and low resource communication. We model the system as a continuous-time<br />
Markov chain, and analyze it by posing a number of questions shedding light<br />
on its behaviour. The properties we are interested in are expressed in continuous<br />
stochastic logic, and probabilistic model checker Prism is used in the analysis.<br />
===<br />
<br />
=== Submission 5 ===<br />
Corresponding Author: Erik de Vink <evink@win.tue.nl><br />
Title: Towards Dynamic Adaptation of Probabilistic Systems<br />
Authors: Erik de Vink, Suzana Andova, and Luuk Groenewegen<br />
<br />
Dynamic system adaptation is modeled in Paradigm as coordination of<br />
collaborating components. A special component McPal allows for addition<br />
of new behavior, of new constraints and of new control in view of a new<br />
collaboration. McPal gradually adapts the system dynamics. It is shown<br />
that the approach also applies to the probabilistic setting. For a<br />
client-server example, where McPal gradually adds probabilistic behavior<br />
to deterministic components, precise modeling of changing system<br />
dynamics is achieved. This modeling of the transient behavior, spanning<br />
the complete migration range from as-is collaboration to to-be collabo-<br />
ration, serves as a stepping stone for quantitative analysis of the<br />
system during adaptation.<br />
===<br />
<br />
=== Submission 6 ===<br />
Corresponding Author: Fuyuan Zhang <fuzh@imm.dtu.dk><br />
Title: Model Checking is Static Analysis<br />
Authors: Fuyuan Zhang and Piotr Filipiuk<br />
<br />
The link between model checking and static analysis has been of great interest<br />
to academia for many years. Early work of Bernhard Steffen and David Schmidt<br />
has shown that classic data-flow analysis is an instance of model checking. The<br />
poster gives an overview of our research aiming to show that also model checking<br />
is static analysis of modal logics and that model checking can be carried by the<br />
static analysis engine; namely ALFP suite. We use Flow Logic, which is a<br />
state-of-the-art approach to static analysis that bridges the gap between a number<br />
of approaches to static analysis including Data Flow Analysis, Constraint Based<br />
Analysis, Abstract Interpretation and Type and Effect Systems. In the developments<br />
it has been demonstrated that Flow Logic is a robust approach that is able to deal<br />
with a variety of calculi, programming languages and recently modal logics such as<br />
CTL, ACTL and alternation-free mu-calculus. In order to calculate the analysis<br />
solution, we use ALFP Suite that computes the least model guaranteed by the Moore<br />
family theorem for ALFP. In its current version, the suite supports two solvers, one<br />
being a differential worklist solver that is based on a representation of relations as<br />
prefix trees and the other being a solver in continuation passing style that is based<br />
on a BDD representation of relations.<br />
===<br />
<br />
=== Submission 7 ===<br />
Corresponding Author: Vashti Galpin <Vashti.Galpin@ed.ac.uk><br />
Title: A Stochastic Hybrid Process Algebra<br />
Authors: Vashti Galpin, Jane Hillston, and Luca Bortolussi<br />
<br />
The process algebra HYPE was developed to model hybrid systems which are<br />
those systems that exhibit both discrete and continuous behaviour. Our new<br />
process algebra extends HYPE by including the ability to model stochastic<br />
behaviour.<br />
<br />
The poster will introduce stochastic HYPE, minimising notational overhead and<br />
through the use of a networking example. It will also contain graphs describing<br />
the evolution of the example over time based on stochastic simulation.<br />
===<br />
<br />
=== Submission 8 ===<br />
Corresponding Author: Arnaud Jobin <arnaud.jobin@irisa.fr><br />
Title: A Linear Operator Framework for Analysing Resource Usage<br />
Authors: David Cachera, Thomas Jensen, Arnaud Jobin, and Pascal Sotin<br />
<br />
We present a semantics-based framework for analysing the quantitative<br />
behaviour of programs with regard to resource usage. We start from an<br />
operational semantics in which costs are modelled using a dioid<br />
structure, which generalizes the classical (max,plus) semiring<br />
structure over reals. The dioid structure of costs allows for defining<br />
the quantitative semantics as a linear operator. We then develop an<br />
approximation framework of such a semantics in order to effectively<br />
compute global cost information from the program. We show how this<br />
framework is related to, and thus can benefit from, the theory of<br />
abstract interpretation for analyzing qualitative properties, We focus<br />
on the notion of long-run cost which models the asymptotic average<br />
cost of a program, and show that our abstraction technique provides a<br />
correct approximation of the concrete long-run cost. We illustrate our<br />
approach on an application example devoted to the computation of<br />
energy consumption for a language with complex array operations and<br />
explicit energy modes management.<br />
===<br />
<br />
=== Submission 9 ===<br />
Corresponding Author: Christoffer Sloth <csloth@cs.aau.dk><br />
Title: Verification of Continuous Dynamical Systems by Timed Automata<br />
Authors: Christoffer Sloth and Rafael Wisniewski<br />
<br />
The poster outlines a method for abstracting continuous dynamical systems by finite<br />
timed automata, which allows automatic verification of continuous systems. The novelty<br />
of the method is that the abstraction is generated from a partition of state space which<br />
is generated by intersecting set-differences of positive invariant sets.<br />
<br />
It is chosen to abstract continuous systems by timed automata, since tools for efficient<br />
verification of such models exist. Additionally, Lyapunov functions are chosen for<br />
generating the partition, because their sub-level sets are positive invariant; hence, it is<br />
possible to determine a priori if the abstraction is sound or complete. Furthermore, for<br />
certain systems it is possible to approximate the reachable set of the continuous system<br />
arbitrarily close by the timed automaton. The structure added to the abstraction by<br />
partitioning the state space by positive invariant sets allows the timed automaton to be<br />
composed of multiple timed automata. This makes it possible to parallelize the verification<br />
process of the timed automaton.<br />
<br />
Some methods require explicit solutions of the differential equations that describe the<br />
continuous dynamics, which are usually unknown. Therefore, the proposed method only<br />
relies on the Lyapunov functions and their derivatives, which can be calculated.<br />
<br />
The proposed abstraction is applied to an example, which illustrates how sound and<br />
complete abstractions are generated.<br />
===<br />
<br />
=== Submission 10 ===<br />
Corresponding Author: Lei Song <leis@itu.dk><br />
Title: A Broadcast Based Stochastic Calculus<br />
Authors: Lei Song, Flemming Nielson, and Bo Friis Nielson<br />
<br />
In our current work we give a stochastic calculus based on broadcast communication. Only<br />
broadcast actions are associated with rates while all the reception actions are passive and<br />
assigned with weights. By doing so there is no need to handle synchronisation between<br />
actions with different rates. We also give a label transition system of our calculus from<br />
which we can get a CTMC naturally. We show the usefulness of our calculus by giving<br />
several examples from performance analysis setting such as batch Markovian arrival<br />
process (BMAP), marked markovian arrival process (MMAP) and closed queueing networks.<br />
===<br />
<br />
=== Submission 11 ===<br />
Corresponding Author: Massimo Callisto <massimo.callisto@unicam.it><br />
Title: Tailoring the Shape Calculus for Quantitative Analysis<br />
Authors: Massimo Callisto De Donato, Flavio Corradini, Maria Rita Di Berardini, Emanuela Merelli, and Luca Tesei<br />
<br />
The Shape Calculus, a bio-inspired language, is a non-deterministic calculus in which processes<br />
are composed of a 3D shape moving in a space and of a behaviour. A process behaviour is formally<br />
expressed as a CCS-like process algebra with deterministic time where channels - the active sites -<br />
are particular surfaces of the shape. A site can bind, after a proper collision, to another compatible<br />
channel forming a more complex shape and a new process. Contextually to the introduction of the<br />
Shape Calculus we defined BioShape, an environment in which a network of Shape Calculus processes,<br />
together with more specific information about motion and behaviour, can be simulated. In particular,<br />
we showed that such a tool is suitable for representing a biological phenomenon at different spatial<br />
and temporal scales and can be used to perform in silico experiments.<br />
<br />
Our aim is to complete the Shape Calculus by providing verification techniques at specification level.<br />
The objective is to find the right abstractions and boundaries that permit the application of existing<br />
quantitative model checking or quantitative equivalence checking techniques to the evolution of a<br />
given network of Shape Calculus processes. Also suitable logic languages for specifying the properties<br />
must be identified. In such a way we target to improve Shape Calculus to promote a coupling between<br />
the calculus and the BioShape tool to work in synergy towards the gaining of quantitative information<br />
about simulated environments.<br />
===</div>Nataliyahttps://wiki.ercim.eu/wg/MLQA/index.php?title=Poster_Session_at_MLQA_2010&diff=283Poster Session at MLQA 20102010-07-16T12:51:57Z<p>Nataliya: </p>
<hr />
<div>__NOTOC__<br />
We invited posters under two categories:<br />
<br />
* Presentation of recent or on-going work relating to models, logics, tools, and/or applications with respect to discrete, stochastic and/or continuous systems and properties.<br />
<br />
* Overview of the recent research activities of a group, in relation to the themes of MLQA.<br />
<br />
There were 11 poster submissions to the MLQA poster session. Click on a poster title in order to access the correspondent poster submission in the pdf format.<br />
<br />
MLQA 2010 - Poster Abstracts<br />
<br />
=== Submission 1 ===<br />
Corresponding Author: Daniel Wagner <d.wagner06@imperial.ac.uk><br />
Title: p-Automata Approach to Probabilistic Verification<br />
Authors: Michael Huth, Nir Piterman, Daniel Wagner<br />
<br />
The poster introduces an automata based approach to the<br />
verification of probabilistic systems. Our so-called<br />
p-automata combine the combinatorial structure of alternating<br />
tree automata with the ability to quantify probabilities of<br />
regular sets of paths. These foundations enable abstraction-based<br />
probabilistic model checking for probabilistic specifications<br />
that subsume Markov chains, PCTL, LTL and CTL* like logics.<br />
<br />
The poster is based on results from "New Foundations for<br />
Discrete-Time Probabilistic Verification" to appear in<br />
Proceedings of QEST 2010.<br />
===<br />
<br />
=== Submission 2 ===<br />
Corresponding Author: N/A<br />
Title: Abstraction of Stochastic Process Algebras<br />
Authors: Nataliya Skrypnyuk, Michael Smith<br />
<br />
Stochastic process algebras are compositional modelling languages<br />
that can be used to describe systems whose behaviour evolves<br />
probabilistically over time - from distributed computer systems, to<br />
signalling pathways in cells. Two such languages are Interactive<br />
Markov Chains (IMC), and the Performance Evaluation Process Algebra<br />
(PEPA), which handle synchronisation between model components in<br />
different ways. The semantics of PEPA can be described as a continuous<br />
time Markov chain (CTMC), whereas for IMC it is a continuous time<br />
Markov decision process (CTMDP).<br />
<br />
In both PEPA and IMC, it is very easy to write a model whose state space<br />
is exponentially larger than its description. It is therefore important to<br />
look for ways to abstract such models, so that they can become small<br />
enough to analyse. Importantly, we want to perform the abstraction at<br />
the language level, so that we maintain the compositionality of the model.<br />
In this poster, we illustrate two different approaches to this - abstraction<br />
of IMC using pathway analysis (a type of static analysis), and abstraction<br />
of PEPA using compositional aggregation of states.<br />
===<br />
<br />
=== Submission 3 ===<br />
Corresponding Author: Igor Cappello <cappello@disi.unitn.it><br />
Title: Quantitative Assessment of Web Services: Applying SCOWS to a Real-Life Scenario<br />
Authors: Igor Cappello and Paola Quaglia<br />
<br />
We present an example of application of SCOWS to a real-life scenario<br />
(loan request) developed within the SENSORIA European Project. SCOWS<br />
is a stochastic process algebra tailored for the purpose of<br />
quantitative assessment of Web Services: applying the labelled<br />
semantics to a SCOWS service S, it is possible to derive the Labelled<br />
Transition System (LTS) representing all the possible behaviours of S.<br />
The LTS can then be used to generate a CTMC on which quantitative<br />
model checking can take place.<br />
<br />
In order to automatically derive the LTS and minimize the state space<br />
needed to represent it, we implemented SCOWS_lts, a tool written in<br />
Java whose output can be imported in a model checker (e.g. PRISM) and<br />
used to perform quantitative analysis.<br />
<br />
We report some results obtained assessing the impact of one parameter<br />
(the rate at which a clerk processes the submitted loan request) on<br />
the overall performance of the service.<br />
===<br />
<br />
=== Submission 4 ===<br />
Corresponding Author: Ender Yüksel <ey@imm.dtu.dk><br />
Title: High Security at a Low Cost<br />
Authors: Ender Yüksel, Hanne Riis Nielson, and Flemming Nielson<br />
<br />
In the future tiny devices with microcontrollers and sensors will be in charge<br />
of numerous activities in our lives. Tracking our energy consumption and CO2<br />
emission, controlling our living conditions, enforcing security, and monitoring<br />
our health will be some examples of their functions These devices will form<br />
wireless networks to communicate with one another, moreover their power<br />
consumption will be very low. It is not hard to predict that our modern society<br />
will depend on the correct operation of these devices, and the security of the<br />
network they are operating.<br />
<br />
Such sensor-based systems, also known as "cyber-physical systems", achieve<br />
security by means of cryptographic protocols. In a simplistic setting where the<br />
power consumption should be minimum and the processing power is limited, it<br />
is more likely that all devices in the network will share the same cryptographic<br />
key. In this study, we are working on the trade-off between two challenges: <br />
"the cryptographic key should be changed frequently to preserve security" and<br />
"the cryptographic key should be changed rarely to save power". We work on the<br />
ZigBee wireless sensor network standard, that offers the advantages of simple<br />
and low resource communication. We model the system as a continuous-time<br />
Markov chain, and analyze it by posing a number of questions shedding light<br />
on its behaviour. The properties we are interested in are expressed in continuous<br />
stochastic logic, and probabilistic model checker Prism is used in the analysis.<br />
===<br />
<br />
=== Submission 5 ===<br />
Corresponding Author: Erik de Vink <evink@win.tue.nl><br />
Title: Towards Dynamic Adaptation of Probabilistic Systems<br />
Authors: Erik de Vink, Suzana Andova, and Luuk Groenewegen<br />
<br />
Dynamic system adaptation is modeled in Paradigm as coordination of<br />
collaborating components. A special component McPal allows for addition<br />
of new behavior, of new constraints and of new control in view of a new<br />
collaboration. McPal gradually adapts the system dynamics. It is shown<br />
that the approach also applies to the probabilistic setting. For a<br />
client-server example, where McPal gradually adds probabilistic behavior<br />
to deterministic components, precise modeling of changing system<br />
dynamics is achieved. This modeling of the transient behavior, spanning<br />
the complete migration range from as-is collaboration to to-be collabo-<br />
ration, serves as a stepping stone for quantitative analysis of the<br />
system during adaptation.<br />
===<br />
<br />
=== Submission 6 ===<br />
Corresponding Author: Fuyuan Zhang <fuzh@imm.dtu.dk><br />
Title: Model Checking is Static Analysis<br />
Authors: Fuyuan Zhang and Piotr Filipiuk<br />
<br />
The link between model checking and static analysis has been of great interest<br />
to academia for many years. Early work of Bernhard Steffen and David Schmidt<br />
has shown that classic data-flow analysis is an instance of model checking. The<br />
poster gives an overview of our research aiming to show that also model checking<br />
is static analysis of modal logics and that model checking can be carried by the<br />
static analysis engine; namely ALFP suite. We use Flow Logic, which is a<br />
state-of-the-art approach to static analysis that bridges the gap between a number<br />
of approaches to static analysis including Data Flow Analysis, Constraint Based<br />
Analysis, Abstract Interpretation and Type and Effect Systems. In the developments<br />
it has been demonstrated that Flow Logic is a robust approach that is able to deal<br />
with a variety of calculi, programming languages and recently modal logics such as<br />
CTL, ACTL and alternation-free mu-calculus. In order to calculate the analysis<br />
solution, we use ALFP Suite that computes the least model guaranteed by the Moore<br />
family theorem for ALFP. In its current version, the suite supports two solvers, one<br />
being a differential worklist solver that is based on a representation of relations as<br />
prefix trees and the other being a solver in continuation passing style that is based<br />
on a BDD representation of relations.<br />
===<br />
<br />
=== Submission 7 ===<br />
Corresponding Author: Vashti Galpin <Vashti.Galpin@ed.ac.uk><br />
Title: A Stochastic Hybrid Process Algebra<br />
Authors: Vashti Galpin, Jane Hillston, and Luca Bortolussi<br />
<br />
The process algebra HYPE was developed to model hybrid systems which are<br />
those systems that exhibit both discrete and continuous behaviour. Our new<br />
process algebra extends HYPE by including the ability to model stochastic<br />
behaviour.<br />
<br />
The poster will introduce stochastic HYPE, minimising notational overhead and<br />
through the use of a networking example. It will also contain graphs describing<br />
the evolution of the example over time based on stochastic simulation.<br />
===<br />
<br />
=== Submission 8 ===<br />
Corresponding Author: Arnaud Jobin <arnaud.jobin@irisa.fr><br />
Title: A Linear Operator Framework for Analysing Resource Usage<br />
Authors: David Cachera, Thomas Jensen, Arnaud Jobin, and Pascal Sotin<br />
<br />
We present a semantics-based framework for analysing the quantitative<br />
behaviour of programs with regard to resource usage. We start from an<br />
operational semantics in which costs are modelled using a dioid<br />
structure, which generalizes the classical (max,plus) semiring<br />
structure over reals. The dioid structure of costs allows for defining<br />
the quantitative semantics as a linear operator. We then develop an<br />
approximation framework of such a semantics in order to effectively<br />
compute global cost information from the program. We show how this<br />
framework is related to, and thus can benefit from, the theory of<br />
abstract interpretation for analyzing qualitative properties, We focus<br />
on the notion of long-run cost which models the asymptotic average<br />
cost of a program, and show that our abstraction technique provides a<br />
correct approximation of the concrete long-run cost. We illustrate our<br />
approach on an application example devoted to the computation of<br />
energy consumption for a language with complex array operations and<br />
explicit energy modes management.<br />
===<br />
<br />
=== Submission 9 ===<br />
Corresponding Author: Christoffer Sloth <csloth@cs.aau.dk><br />
Title: Verification of Continuous Dynamical Systems by Timed Automata<br />
Authors: Christoffer Sloth and Rafael Wisniewski<br />
<br />
The poster outlines a method for abstracting continuous dynamical systems by finite<br />
timed automata, which allows automatic verification of continuous systems. The novelty<br />
of the method is that the abstraction is generated from a partition of state space which<br />
is generated by intersecting set-differences of positive invariant sets.<br />
<br />
It is chosen to abstract continuous systems by timed automata, since tools for efficient<br />
verification of such models exist. Additionally, Lyapunov functions are chosen for<br />
generating the partition, because their sub-level sets are positive invariant; hence, it is<br />
possible to determine a priori if the abstraction is sound or complete. Furthermore, for<br />
certain systems it is possible to approximate the reachable set of the continuous system<br />
arbitrarily close by the timed automaton. The structure added to the abstraction by<br />
partitioning the state space by positive invariant sets allows the timed automaton to be<br />
composed of multiple timed automata. This makes it possible to parallelize the verification<br />
process of the timed automaton.<br />
<br />
Some methods require explicit solutions of the differential equations that describe the<br />
continuous dynamics, which are usually unknown. Therefore, the proposed method only<br />
relies on the Lyapunov functions and their derivatives, which can be calculated.<br />
<br />
The proposed abstraction is applied to an example, which illustrates how sound and<br />
complete abstractions are generated.<br />
===<br />
<br />
=== Submission 10 ===<br />
Corresponding Author: Lei Song <leis@itu.dk><br />
Title: A Broadcast Based Stochastic Calculus<br />
Authors: Lei Song, Flemming Nielson, and Bo Friis Nielson<br />
<br />
In our current work we give a stochastic calculus based on broadcast communication. Only<br />
broadcast actions are associated with rates while all the reception actions are passive and<br />
assigned with weights. By doing so there is no need to handle synchronisation between<br />
actions with different rates. We also give a label transition system of our calculus from<br />
which we can get a CTMC naturally. We show the usefulness of our calculus by giving<br />
several examples from performance analysis setting such as batch Markovian arrival<br />
process (BMAP), marked markovian arrival process (MMAP) and closed queueing networks.<br />
===<br />
<br />
=== Submission 11 ===<br />
Corresponding Author: Massimo Callisto <massimo.callisto@unicam.it><br />
Title: Tailoring the Shape Calculus for Quantitative Analysis<br />
Authors: Massimo Callisto De Donato, Flavio Corradini, Maria Rita Di Berardini, Emanuela Merelli, and Luca Tesei<br />
<br />
The Shape Calculus, a bio-inspired language, is a non-deterministic calculus in which processes<br />
are composed of a 3D shape moving in a space and of a behaviour. A process behaviour is formally<br />
expressed as a CCS-like process algebra with deterministic time where channels - the active sites -<br />
are particular surfaces of the shape. A site can bind, after a proper collision, to another compatible<br />
channel forming a more complex shape and a new process. Contextually to the introduction of the<br />
Shape Calculus we defined BioShape, an environment in which a network of Shape Calculus processes,<br />
together with more specific information about motion and behaviour, can be simulated. In particular,<br />
we showed that such a tool is suitable for representing a biological phenomenon at different spatial<br />
and temporal scales and can be used to perform in silico experiments.<br />
<br />
Our aim is to complete the Shape Calculus by providing verification techniques at specification level.<br />
The objective is to find the right abstractions and boundaries that permit the application of existing<br />
quantitative model checking or quantitative equivalence checking techniques to the evolution of a<br />
given network of Shape Calculus processes. Also suitable logic languages for specifying the properties<br />
must be identified. In such a way we target to improve Shape Calculus to promote a coupling between<br />
the calculus and the BioShape tool to work in synergy towards the gaining of quantitative information<br />
about simulated environments.<br />
===</div>Nataliya