Search | arXiv e-print repository

<!DOCTYPE html> <html lang="en"> <head> <meta charset="utf-8"/> <meta name="viewport" content="width=device-width, initial-scale=1"/>  <link rel="apple-touch-icon" sizes="180x180" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/apple-touch-icon.png"> <link rel="icon" type="image/png" sizes="32x32" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/favicon-32x32.png"> <link rel="icon" type="image/png" sizes="16x16" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/favicon-16x16.png"> <link rel="manifest" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/site.webmanifest"> <link rel="mask-icon" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/safari-pinned-tab.svg" color="#b31b1b"> <link rel="shortcut icon" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/favicon.ico"> <meta name="msapplication-TileColor" content="#b31b1b"> <meta name="msapplication-config" content="images/icons/browserconfig.xml"> <meta name="theme-color" content="#b31b1b">  <title>Search | arXiv e-print repository</title> <script defer src="https://static.arxiv.org/static/base/1.0.0a5/fontawesome-free-5.11.2-web/js/all.js"></script> <link rel="stylesheet" href="https://static.arxiv.org/static/base/1.0.0a5/css/arxivstyle.css" /> <script type="text/x-mathjax-config"> MathJax.Hub.Config({ messageStyle: "none", extensions: ["tex2jax.js"], jax: ["input/TeX", "output/HTML-CSS"], tex2jax: { inlineMath: [ ['$','$'], ["\$","\$"] ], displayMath: [ ['$$','$$'], ["\\[","\\]"] ], processEscapes: true, ignoreClass: '.*', processClass: 'mathjax.*' }, TeX: { extensions: ["AMSmath.js", "AMSsymbols.js", "noErrors.js"], noErrors: { inlineDelimiters: ["$","$"], multiLine: false, style: { "font-size": "normal", "border": "" } } }, "HTML-CSS": { availableFonts: ["TeX"] } }); </script> <script src='//static.arxiv.org/MathJax-2.7.3/MathJax.js'></script> <script src="https://static.arxiv.org/static/base/1.0.0a5/js/notification.js"></script> <link rel="stylesheet" href="https://static.arxiv.org/static/search/0.5.6/css/bulma-tooltip.min.css" /> <link rel="stylesheet" href="https://static.arxiv.org/static/search/0.5.6/css/search.css" /> <script src="https://code.jquery.com/jquery-3.2.1.slim.min.js" integrity="sha256-k2WSCIexGzOj3Euiig+TlR8gA0EmPjuc79OEeY5L45g=" crossorigin="anonymous"></script> <script src="https://static.arxiv.org/static/search/0.5.6/js/fieldset.js"></script> <style> radio#cf-customfield_11400 { display: none; } </style> </head> <body> <header><a href="#main-container" class="is-sr-only">Skip to main content</a>  <div class="attribution level is-marginless" role="banner"> <div class="level-left"> <a class="level-item" href="https://cornell.edu/"><img src="https://static.arxiv.org/static/base/1.0.0a5/images/cornell-reduced-white-SMALL.svg" alt="Cornell University" width="200" aria-label="logo" /></a> </div> <div class="level-right is-marginless"><p class="sponsors level-item is-marginless"><span id="support-ack-url">We gratefully acknowledge support from<br /> the Simons Foundation, <a href="https://info.arxiv.org/about/ourmembers.html">member institutions</a>, and all contributors. <a href="https://info.arxiv.org/about/donate.html">Donate</a></span></p></div> </div>  <div class="identity level is-marginless"> <div class="level-left"> <div class="level-item"> <a class="arxiv" href="https://arxiv.org/" aria-label="arxiv-logo"> <img src="https://static.arxiv.org/static/base/1.0.0a5/images/arxiv-logo-one-color-white.svg" aria-label="logo" alt="arxiv logo" width="85" style="width:85px;"/> </a> </div> </div> <div class="search-block level-right"> <form class="level-item mini-search" method="GET" action="https://arxiv.org/search"> <div class="field has-addons"> <div class="control"> <input class="input is-small" type="text" name="query" placeholder="Search..." aria-label="Search term or terms" /> <p class="help"><a href="https://info.arxiv.org/help">Help</a> | <a href="https://arxiv.org/search/advanced">Advanced Search</a></p> </div> <div class="control"> <div class="select is-small"> <select name="searchtype" aria-label="Field to search"> <option value="all" selected="selected">All fields</option> <option value="title">Title</option> <option value="author">Author</option> <option value="abstract">Abstract</option> <option value="comments">Comments</option> <option value="journal_ref">Journal reference</option> <option value="acm_class">ACM classification</option> <option value="msc_class">MSC classification</option> <option value="report_num">Report number</option> <option value="paper_id">arXiv identifier</option> <option value="doi">DOI</option> <option value="orcid">ORCID</option> <option value="author_id">arXiv author ID</option> <option value="help">Help pages</option> <option value="full_text">Full text</option> </select> </div> </div> <input type="hidden" name="source" value="header"> <button class="button is-small is-cul-darker">Search</button> </div> </form> </div> </div>  <div class="container"> <div class="user-tools is-size-7 has-text-right has-text-weight-bold" role="navigation" aria-label="User menu"> <a href="https://arxiv.org/login">Login</a> </div> </div> </header> <main class="container" id="main-container"> <div class="level is-marginless"> <div class="level-left"> <h1 class="title is-clearfix"> Showing 1–33 of 33 results for author: <span class="mathjax">Calinescu, R</span> </h1> </div> <div class="level-right is-hidden-mobile">  <span class="help" style="display: inline-block;"><a href="https://github.com/arXiv/arxiv-search/releases">Search v0.5.6 released 2020-02-24</a>  </span> </div> </div> <div class="content"> <form method="GET" action="/search/cs" aria-role="search"> Searching in archive <strong>cs</strong>. <a href="/search/?searchtype=author&query=Calinescu%2C+R">Search in all archives.</a> <div class="field has-addons-tablet"> <div class="control is-expanded"> <label for="query" class="hidden-label">Search term or terms</label> <input class="input is-medium" id="query" name="query" placeholder="Search term..." type="text" value="Calinescu, R"> </div> <div class="select control is-medium"> <label class="is-hidden" for="searchtype">Field</label> <select class="is-medium" id="searchtype" name="searchtype"><option value="all">All fields</option><option value="title">Title</option><option selected value="author">Author(s)</option><option value="abstract">Abstract</option><option value="comments">Comments</option><option value="journal_ref">Journal reference</option><option value="acm_class">ACM classification</option><option value="msc_class">MSC classification</option><option value="report_num">Report number</option><option value="paper_id">arXiv identifier</option><option value="doi">DOI</option><option value="orcid">ORCID</option><option value="license">License (URI)</option><option value="author_id">arXiv author ID</option><option value="help">Help pages</option><option value="full_text">Full text</option></select> </div> <div class="control"> <button class="button is-link is-medium">Search</button> </div> </div> <div class="field"> <div class="control is-size-7"> <label class="radio"> <input checked id="abstracts-0" name="abstracts" type="radio" value="show"> Show abstracts </label> <label class="radio"> <input id="abstracts-1" name="abstracts" type="radio" value="hide"> Hide abstracts </label> </div> </div> <div class="is-clearfix" style="height: 2.5em"> <div class="is-pulled-right"> <a href="/search/advanced?terms-0-term=Calinescu%2C+R&terms-0-field=author&size=50&order=-announced_date_first">Advanced Search</a> </div> </div> <input type="hidden" name="order" value="-announced_date_first"> <input type="hidden" name="size" value="50"> </form> <div class="level breathe-horizontal"> <div class="level-left"> <form method="GET" action="/search/"> <div style="display: none;"> <select id="searchtype" name="searchtype"><option value="all">All fields</option><option value="title">Title</option><option selected value="author">Author(s)</option><option value="abstract">Abstract</option><option value="comments">Comments</option><option value="journal_ref">Journal reference</option><option value="acm_class">ACM classification</option><option value="msc_class">MSC classification</option><option value="report_num">Report number</option><option value="paper_id">arXiv identifier</option><option value="doi">DOI</option><option value="orcid">ORCID</option><option value="license">License (URI)</option><option value="author_id">arXiv author ID</option><option value="help">Help pages</option><option value="full_text">Full text</option></select> <input id="query" name="query" type="text" value="Calinescu, R"> <ul id="abstracts"><li><input checked id="abstracts-0" name="abstracts" type="radio" value="show"> <label for="abstracts-0">Show abstracts</label></li><li><input id="abstracts-1" name="abstracts" type="radio" value="hide"> <label for="abstracts-1">Hide abstracts</label></li></ul> </div> <div class="box field is-grouped is-grouped-multiline level-item"> <div class="control"> <span class="select is-small"> <select id="size" name="size"><option value="25">25</option><option selected value="50">50</option><option value="100">100</option><option value="200">200</option></select> </span> <label for="size">results per page</label>. </div> <div class="control"> <label for="order">Sort results by</label> <span class="select is-small"> <select id="order" name="order"><option selected value="-announced_date_first">Announcement date (newest first)</option><option value="announced_date_first">Announcement date (oldest first)</option><option value="-submitted_date">Submission date (newest first)</option><option value="submitted_date">Submission date (oldest first)</option><option value="">Relevance</option></select> </span> </div> <div class="control"> <button class="button is-small is-link">Go</button> </div> </div> </form> </div> </div> <ol class="breathe-horizontal" start="1"> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2405.18180">arXiv:2405.18180</a> <span> [<a href="https://arxiv.org/pdf/2405.18180">pdf</a>, <a href="https://arxiv.org/format/2405.18180">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Artificial Intelligence">cs.AI</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> </div> </div> <p class="title is-5 mathjax"> Safe Reinforcement Learning in Black-Box Environments via Adaptive Shielding </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bethell%2C+D">Daniel Bethell</a>, <a href="/search/cs?searchtype=author&query=Gerasimou%2C+S">Simos Gerasimou</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Imrie%2C+C">Calum Imrie</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2405.18180v1-abstract-short" style="display: inline;"> Empowering safe exploration of reinforcement learning (RL) agents during training is a critical impediment towards deploying RL agents in many real-world scenarios. Training RL agents in unknown, black-box environments poses an even greater safety risk when prior knowledge of the domain/task is unavailable. We introduce ADVICE (Adaptive Shielding with a Contrastive Autoencoder), a novel post-shiel… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2405.18180v1-abstract-full').style.display = 'inline'; document.getElementById('2405.18180v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2405.18180v1-abstract-full" style="display: none;"> Empowering safe exploration of reinforcement learning (RL) agents during training is a critical impediment towards deploying RL agents in many real-world scenarios. Training RL agents in unknown, black-box environments poses an even greater safety risk when prior knowledge of the domain/task is unavailable. We introduce ADVICE (Adaptive Shielding with a Contrastive Autoencoder), a novel post-shielding technique that distinguishes safe and unsafe features of state-action pairs during training, thus protecting the RL agent from executing actions that yield potentially hazardous outcomes. Our comprehensive experimental evaluation against state-of-the-art safe RL exploration techniques demonstrates how ADVICE can significantly reduce safety violations during training while maintaining a competitive outcome reward. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2405.18180v1-abstract-full').style.display = 'none'; document.getElementById('2405.18180v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 28 May, 2024; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> May 2024. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2404.12335">arXiv:2404.12335</a> <span> [<a href="https://arxiv.org/pdf/2404.12335">pdf</a>, <a href="https://arxiv.org/format/2404.12335">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> </div> <p class="title is-5 mathjax"> Normative Requirements Operationalization with Large Language Models </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Feng%2C+N">Nick Feng</a>, <a href="/search/cs?searchtype=author&query=Marsso%2C+L">Lina Marsso</a>, <a href="/search/cs?searchtype=author&query=Yaman%2C+S+G">S. Getir Yaman</a>, <a href="/search/cs?searchtype=author&query=Standen%2C+I">Isobel Standen</a>, <a href="/search/cs?searchtype=author&query=Baatartogtokh%2C+Y">Yesugen Baatartogtokh</a>, <a href="/search/cs?searchtype=author&query=Ayad%2C+R">Reem Ayad</a>, <a href="/search/cs?searchtype=author&query=de+Mello%2C+V+O">Vict贸ria Oldemburgo de Mello</a>, <a href="/search/cs?searchtype=author&query=Townsend%2C+B">Bev Townsend</a>, <a href="/search/cs?searchtype=author&query=Bartels%2C+H">Hanne Bartels</a>, <a href="/search/cs?searchtype=author&query=Cavalcanti%2C+A">Ana Cavalcanti</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Chechik%2C+M">Marsha Chechik</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2404.12335v2-abstract-short" style="display: inline;"> Normative non-functional requirements specify constraints that a system must observe in order to avoid violations of social, legal, ethical, empathetic, and cultural norms. As these requirements are typically defined by non-technical system stakeholders with different expertise and priorities (ethicists, lawyers, social scientists, etc.), ensuring their well-formedness and consistency is very chal… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2404.12335v2-abstract-full').style.display = 'inline'; document.getElementById('2404.12335v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2404.12335v2-abstract-full" style="display: none;"> Normative non-functional requirements specify constraints that a system must observe in order to avoid violations of social, legal, ethical, empathetic, and cultural norms. As these requirements are typically defined by non-technical system stakeholders with different expertise and priorities (ethicists, lawyers, social scientists, etc.), ensuring their well-formedness and consistency is very challenging. Recent research has tackled this challenge using a domain-specific language to specify normative requirements as rules whose consistency can then be analysed with formal methods. In this paper, we propose a complementary approach that uses Large Language Models to extract semantic relationships between abstract representations of system capabilities. These relations, which are often assumed implicitly by non-technical stakeholders (e.g., based on common sense or domain knowledge), are then used to enrich the automated reasoning techniques for eliciting and analyzing the consistency of normative requirements. We show the effectiveness of our approach to normative requirements elicitation and operationalization through a range of real-world case studies. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2404.12335v2-abstract-full').style.display = 'none'; document.getElementById('2404.12335v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 28 May, 2024; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 18 April, 2024; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> April 2024. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2401.17187">arXiv:2401.17187</a> <span> [<a href="https://arxiv.org/pdf/2401.17187">pdf</a>, <a href="https://arxiv.org/format/2401.17187">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> </div> <p class="title is-5 mathjax"> Formal Synthesis of Uncertainty Reduction Controllers </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Carwehl%2C+M">Marc Carwehl</a>, <a href="/search/cs?searchtype=author&query=Imrie%2C+C">Calum Imrie</a>, <a href="/search/cs?searchtype=author&query=Vogel%2C+T">Thomas Vogel</a>, <a href="/search/cs?searchtype=author&query=Rodrigues%2C+G">Gena铆na Rodrigues</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Grunske%2C+L">Lars Grunske</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2401.17187v2-abstract-short" style="display: inline;"> In its quest for approaches to taming uncertainty in self-adaptive systems (SAS), the research community has largely focused on solutions that adapt the SAS architecture or behaviour in response to uncertainty. By comparison, solutions that reduce the uncertainty affecting SAS (other than through the blanket monitoring of their components and environment) remain underexplored. Our paper proposes a… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2401.17187v2-abstract-full').style.display = 'inline'; document.getElementById('2401.17187v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2401.17187v2-abstract-full" style="display: none;"> In its quest for approaches to taming uncertainty in self-adaptive systems (SAS), the research community has largely focused on solutions that adapt the SAS architecture or behaviour in response to uncertainty. By comparison, solutions that reduce the uncertainty affecting SAS (other than through the blanket monitoring of their components and environment) remain underexplored. Our paper proposes a more nuanced, adaptive approach to SAS uncertainty reduction. To that end, we introduce a SAS architecture comprising an uncertainty reduction controller that drives the adaptive acquisition of new information within the SAS adaptation loop, and a tool-supported method that uses probabilistic model checking to synthesise such controllers. The controllers generated by our method deliver optimal trade-offs between SAS uncertainty reduction benefits and new information acquisition costs. We illustrate the use and evaluate the effectiveness of our approach for mobile robot navigation and server infrastructure management SAS. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2401.17187v2-abstract-full').style.display = 'none'; document.getElementById('2401.17187v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 1 February, 2024; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 30 January, 2024; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> January 2024. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2401.05673">arXiv:2401.05673</a> <span> [<a href="https://arxiv.org/pdf/2401.05673">pdf</a>, <a href="https://arxiv.org/format/2401.05673">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> <div class="is-inline-block" style="margin-left: 0.5rem"> <div class="tags has-addons"> <span class="tag is-dark is-size-7">doi</span> <span class="tag is-light is-size-7"><a class="" href="https://doi.org/10.1145/3597503.3639093">10.1145/3597503.3639093 <i class="fa fa-external-link" aria-hidden="true"></i></a></span> </div> </div> </div> <p class="title is-5 mathjax"> Analyzing and Debugging Normative Requirements via Satisfiability Checking </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Feng%2C+N">Nick Feng</a>, <a href="/search/cs?searchtype=author&query=Marsso%2C+L">Lina Marsso</a>, <a href="/search/cs?searchtype=author&query=Yaman%2C+S+G">Sinem Getir Yaman</a>, <a href="/search/cs?searchtype=author&query=Baatartogtokh%2C+Y">Yesugen Baatartogtokh</a>, <a href="/search/cs?searchtype=author&query=Ayad%2C+R">Reem Ayad</a>, <a href="/search/cs?searchtype=author&query=de+Mello%2C+V+O">Vict贸ria Oldemburgo de Mello</a>, <a href="/search/cs?searchtype=author&query=Townsend%2C+B">Beverley Townsend</a>, <a href="/search/cs?searchtype=author&query=Standen%2C+I">Isobel Standen</a>, <a href="/search/cs?searchtype=author&query=Stefanakos%2C+I">Ioannis Stefanakos</a>, <a href="/search/cs?searchtype=author&query=Imrie%2C+C">Calum Imrie</a>, <a href="/search/cs?searchtype=author&query=Rodrigues%2C+G+N">Gena铆na Nunes Rodrigues</a>, <a href="/search/cs?searchtype=author&query=Cavalcanti%2C+A">Ana Cavalcanti</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Chechik%2C+M">Marsha Chechik</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2401.05673v1-abstract-short" style="display: inline;"> As software systems increasingly interact with humans in application domains such as transportation and healthcare, they raise concerns related to the social, legal, ethical, empathetic, and cultural (SLEEC) norms and values of their stakeholders. Normative non-functional requirements (N-NFRs) are used to capture these concerns by setting SLEEC-relevant boundaries for system behavior. Since N-NFRs… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2401.05673v1-abstract-full').style.display = 'inline'; document.getElementById('2401.05673v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2401.05673v1-abstract-full" style="display: none;"> As software systems increasingly interact with humans in application domains such as transportation and healthcare, they raise concerns related to the social, legal, ethical, empathetic, and cultural (SLEEC) norms and values of their stakeholders. Normative non-functional requirements (N-NFRs) are used to capture these concerns by setting SLEEC-relevant boundaries for system behavior. Since N-NFRs need to be specified by multiple stakeholders with widely different, non-technical expertise (ethicists, lawyers, regulators, end users, etc.), N-NFR elicitation is very challenging. To address this challenge, we introduce N-Check, a novel tool-supported formal approach to N-NFR analysis and debugging. N-Check employs satisfiability checking to identify a broad spectrum of N-NFR well-formedness issues (WFI), such as conflicts, redundancy, restrictiveness, insufficiency, yielding diagnostics which pinpoint their causes in a user-friendly way that enables non-technical stakeholders to understand and fix them. We show the effectiveness and usability of our approach through nine case studies in which teams of ethicists, lawyers, philosophers, psychologists, safety analysts, and engineers used N-Check to analyse and debug 233 N-NFRs comprising 62 issues for the software underpinning the operation of systems ranging from assistive-care robots and tree-disease detection drones to manufacturing collaborative robots. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2401.05673v1-abstract-full').style.display = 'none'; document.getElementById('2401.05673v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 11 January, 2024; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> January 2024. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2310.19119">arXiv:2310.19119</a> <span> [<a href="https://arxiv.org/pdf/2310.19119">pdf</a>, <a href="https://arxiv.org/format/2310.19119">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Computer Vision and Pattern Recognition">cs.CV</span> </div> </div> <p class="title is-5 mathjax"> Out-of-distribution Object Detection through Bayesian Uncertainty Estimation </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Zhang%2C+T">Tianhao Zhang</a>, <a href="/search/cs?searchtype=author&query=Wang%2C+S">Shenglin Wang</a>, <a href="/search/cs?searchtype=author&query=Bouaynaya%2C+N">Nidhal Bouaynaya</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Mihaylova%2C+L">Lyudmila Mihaylova</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2310.19119v1-abstract-short" style="display: inline;"> The superior performance of object detectors is often established under the condition that the test samples are in the same distribution as the training data. However, in many practical applications, out-of-distribution (OOD) instances are inevitable and usually lead to uncertainty in the results. In this paper, we propose a novel, intuitive, and scalable probabilistic object detection method for… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2310.19119v1-abstract-full').style.display = 'inline'; document.getElementById('2310.19119v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2310.19119v1-abstract-full" style="display: none;"> The superior performance of object detectors is often established under the condition that the test samples are in the same distribution as the training data. However, in many practical applications, out-of-distribution (OOD) instances are inevitable and usually lead to uncertainty in the results. In this paper, we propose a novel, intuitive, and scalable probabilistic object detection method for OOD detection. Unlike other uncertainty-modeling methods that either require huge computational costs to infer the weight distributions or rely on model training through synthetic outlier data, our method is able to distinguish between in-distribution (ID) data and OOD data via weight parameter sampling from proposed Gaussian distributions based on pre-trained networks. We demonstrate that our Bayesian object detector can achieve satisfactory OOD identification performance by reducing the FPR95 score by up to 8.19% and increasing the AUROC score by up to 13.94% when trained on BDD100k and VOC datasets as the ID datasets and evaluated on COCO2017 dataset as the OOD dataset. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2310.19119v1-abstract-full').style.display = 'none'; document.getElementById('2310.19119v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 29 October, 2023; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> October 2023. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Journal ref:</span> 2023 26th International Conference on Information Fusion (FUSION), 1-8, 2023 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2308.09647">arXiv:2308.09647</a> <span> [<a href="https://arxiv.org/pdf/2308.09647">pdf</a>, <a href="https://arxiv.org/format/2308.09647">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Artificial Intelligence">cs.AI</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Machine Learning">stat.ML</span> </div> </div> <p class="title is-5 mathjax"> Robust Uncertainty Quantification Using Conformalised Monte Carlo Prediction </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Bethell%2C+D">Daniel Bethell</a>, <a href="/search/cs?searchtype=author&query=Gerasimou%2C+S">Simos Gerasimou</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2308.09647v2-abstract-short" style="display: inline;"> Deploying deep learning models in safety-critical applications remains a very challenging task, mandating the provision of assurances for the dependable operation of these models. Uncertainty quantification (UQ) methods estimate the model's confidence per prediction, informing decision-making by considering the effect of randomness and model misspecification. Despite the advances of state-of-the-a… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2308.09647v2-abstract-full').style.display = 'inline'; document.getElementById('2308.09647v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2308.09647v2-abstract-full" style="display: none;"> Deploying deep learning models in safety-critical applications remains a very challenging task, mandating the provision of assurances for the dependable operation of these models. Uncertainty quantification (UQ) methods estimate the model's confidence per prediction, informing decision-making by considering the effect of randomness and model misspecification. Despite the advances of state-of-the-art UQ methods, they are computationally expensive or produce conservative prediction sets/intervals. We introduce MC-CP, a novel hybrid UQ method that combines a new adaptive Monte Carlo (MC) dropout method with conformal prediction (CP). MC-CP adaptively modulates the traditional MC dropout at runtime to save memory and computation resources, enabling predictions to be consumed by CP, yielding robust prediction sets/intervals. Throughout comprehensive experiments, we show that MC-CP delivers significant improvements over advanced UQ methods, like MC dropout, RAPS and CQR, both in classification and regression benchmarks. MC-CP can be easily added to existing models, making its deployment simple. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2308.09647v2-abstract-full').style.display = 'none'; document.getElementById('2308.09647v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 22 January, 2024; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 18 August, 2023; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> August 2023. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2307.03697">arXiv:2307.03697</a> <span> [<a href="https://arxiv.org/pdf/2307.03697">pdf</a>, <a href="https://arxiv.org/format/2307.03697">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> </div> <p class="title is-5 mathjax"> Specification, Validation and Verification of Social, Legal, Ethical, Empathetic and Cultural Requirements for Autonomous Agents </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Yaman%2C+S+G">Sinem Getir Yaman</a>, <a href="/search/cs?searchtype=author&query=Cavalcanti%2C+A">Ana Cavalcanti</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Paterson%2C+C">Colin Paterson</a>, <a href="/search/cs?searchtype=author&query=Ribeiro%2C+P">Pedro Ribeiro</a>, <a href="/search/cs?searchtype=author&query=Townsend%2C+B">Beverley Townsend</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2307.03697v1-abstract-short" style="display: inline;"> Autonomous agents are increasingly being proposed for use in healthcare, assistive care, education, and other applications governed by complex human-centric norms. To ensure compliance with these norms, the rules they induce need to be unambiguously defined, checked for consistency, and used to verify the agent. In this paper, we introduce a framework for formal specification, validation and verif… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2307.03697v1-abstract-full').style.display = 'inline'; document.getElementById('2307.03697v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2307.03697v1-abstract-full" style="display: none;"> Autonomous agents are increasingly being proposed for use in healthcare, assistive care, education, and other applications governed by complex human-centric norms. To ensure compliance with these norms, the rules they induce need to be unambiguously defined, checked for consistency, and used to verify the agent. In this paper, we introduce a framework for formal specification, validation and verification of social, legal, ethical, empathetic and cultural (SLEEC) rules for autonomous agents. Our framework comprises: (i) a language for specifying SLEEC rules and rule defeaters (that is, circumstances in which a rule does not apply or an alternative form of the rule is required); (ii) a formal semantics (defined in the process algebra tock-CSP) for the language; and (iii) methods for detecting conflicts and redundancy within a set of rules, and for verifying the compliance of an autonomous agent with such rules. We show the applicability of our framework for two autonomous agents from different domains: a firefighter UAV, and an assistive-dressing robot. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2307.03697v1-abstract-full').style.display = 'none'; document.getElementById('2307.03697v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 7 July, 2023; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> July 2023. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2303.08476">arXiv:2303.08476</a> <span> [<a href="https://arxiv.org/pdf/2303.08476">pdf</a>, <a href="https://arxiv.org/format/2303.08476">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Robotics">cs.RO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Artificial Intelligence">cs.AI</span> </div> </div> <p class="title is-5 mathjax"> Bayesian Learning for the Robust Verification of Autonomous Robots </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Zhao%2C+X">Xingyu Zhao</a>, <a href="/search/cs?searchtype=author&query=Gerasimou%2C+S">Simos Gerasimou</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Imrie%2C+C">Calum Imrie</a>, <a href="/search/cs?searchtype=author&query=Robu%2C+V">Valentin Robu</a>, <a href="/search/cs?searchtype=author&query=Flynn%2C+D">David Flynn</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2303.08476v2-abstract-short" style="display: inline;"> Autonomous robots used in infrastructure inspection, space exploration and other critical missions operate in highly dynamic environments. As such, they must continually verify their ability to complete the tasks associated with these missions safely and effectively. Here we present a Bayesian learning framework that enables this runtime verification of autonomous robots. The framework uses prior… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2303.08476v2-abstract-full').style.display = 'inline'; document.getElementById('2303.08476v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2303.08476v2-abstract-full" style="display: none;"> Autonomous robots used in infrastructure inspection, space exploration and other critical missions operate in highly dynamic environments. As such, they must continually verify their ability to complete the tasks associated with these missions safely and effectively. Here we present a Bayesian learning framework that enables this runtime verification of autonomous robots. The framework uses prior knowledge and observations of the verified robot to learn expected ranges for the occurrence rates of regular and singular (e.g., catastrophic failure) events. Interval continuous-time Markov models defined using these ranges are then analysed to obtain expected intervals of variation for system properties such as mission duration and success probability. We apply the framework to an autonomous robotic mission for underwater infrastructure inspection and repair. The formal proofs and experiments presented in the paper show that our framework produces results that reflect the uncertainty intrinsic to many real-world systems, enabling the robust verification of their quantitative properties under parametric uncertainty. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2303.08476v2-abstract-full').style.display = 'none'; document.getElementById('2303.08476v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 11 December, 2023; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 15 March, 2023; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> March 2023. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Accepted by Communications Engineering</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2302.04634">arXiv:2302.04634</a> <span> [<a href="https://arxiv.org/pdf/2302.04634">pdf</a>, <a href="https://arxiv.org/format/2302.04634">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Computer Vision and Pattern Recognition">cs.CV</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Artificial Intelligence">cs.AI</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Formal Languages and Automata Theory">cs.FL</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> </div> </div> <p class="title is-5 mathjax"> Closed-loop Analysis of Vision-based Autonomous Systems: A Case Study </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Pasareanu%2C+C+S">Corina S. Pasareanu</a>, <a href="/search/cs?searchtype=author&query=Mangal%2C+R">Ravi Mangal</a>, <a href="/search/cs?searchtype=author&query=Gopinath%2C+D">Divya Gopinath</a>, <a href="/search/cs?searchtype=author&query=Yaman%2C+S+G">Sinem Getir Yaman</a>, <a href="/search/cs?searchtype=author&query=Imrie%2C+C">Calum Imrie</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Yu%2C+H">Huafeng Yu</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2302.04634v1-abstract-short" style="display: inline;"> Deep neural networks (DNNs) are increasingly used in safety-critical autonomous systems as perception components processing high-dimensional image data. Formal analysis of these systems is particularly challenging due to the complexity of the perception DNNs, the sensors (cameras), and the environment conditions. We present a case study applying formal probabilistic analysis techniques to an exper… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2302.04634v1-abstract-full').style.display = 'inline'; document.getElementById('2302.04634v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2302.04634v1-abstract-full" style="display: none;"> Deep neural networks (DNNs) are increasingly used in safety-critical autonomous systems as perception components processing high-dimensional image data. Formal analysis of these systems is particularly challenging due to the complexity of the perception DNNs, the sensors (cameras), and the environment conditions. We present a case study applying formal probabilistic analysis techniques to an experimental autonomous system that guides airplanes on taxiways using a perception DNN. We address the above challenges by replacing the camera and the network with a compact probabilistic abstraction built from the confusion matrices computed for the DNN on a representative image data set. We also show how to leverage local, DNN-specific analyses as run-time guards to increase the safety of the overall system. Our findings are applicable to other autonomous systems that use complex DNNs for perception. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2302.04634v1-abstract-full').style.display = 'none'; document.getElementById('2302.04634v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 6 February, 2023; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> February 2023. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2211.17218">arXiv:2211.17218</a> <span> [<a href="https://arxiv.org/pdf/2211.17218">pdf</a>, <a href="https://arxiv.org/format/2211.17218">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> </div> <p class="title is-5 mathjax"> Specification Architectural Viewpoint for Benefit-Cost-Risk-Aware Decision-Making in Self-Adaptive Systems </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Weyns%2C+D">Danny Weyns</a>, <a href="/search/cs?searchtype=author&query=Avegriou%2C+P">Paris Avegriou</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Hezavehi%2C+S+M">Sara M. Hezavehi</a>, <a href="/search/cs?searchtype=author&query=Mirandola%2C+R">Raffaela Mirandola</a>, <a href="/search/cs?searchtype=author&query=Perez-Palacin%2C+D">Diego Perez-Palacin</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2211.17218v1-abstract-short" style="display: inline;"> Over the past two decades, researchers and engineers have extensively studied the problem of how to enable a software system to deal with uncertain operating conditions. One prominent solution to this problem is self-adaptation, which equips a software system with a feedback loop that resolves uncertainties during operation and adapts the system to deal with them when necessary. Most self-adaptati… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2211.17218v1-abstract-full').style.display = 'inline'; document.getElementById('2211.17218v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2211.17218v1-abstract-full" style="display: none;"> Over the past two decades, researchers and engineers have extensively studied the problem of how to enable a software system to deal with uncertain operating conditions. One prominent solution to this problem is self-adaptation, which equips a software system with a feedback loop that resolves uncertainties during operation and adapts the system to deal with them when necessary. Most self-adaptation approaches developed so far use decision-making mechanisms that focus on achieving a set of goals, i.e., that select for execution the adaptation option with the best estimated benefit. A few approaches have also considered the estimated (one-off) cost of executing the candidate adaptation options. We argue that besides benefit and cost, decision-making in self-adaptive systems should also consider the estimated risk the system or its users would be exposed to if an adaptation option were selected for execution. Balancing all three factors when evaluating the options for adaptation when mitigating uncertainty is essential, not only for satisfying the concerns of the stakeholders, but also to ensure safety and public acceptance of self-adaptive systems. In this paper, we present an ISO/IEC/IEEE 42010 compatible architectural viewpoint that considers the estimated benefit, cost, and risk as core factors of each adaptation option considered in self-adaptation. The viewpoint aims to support software architects responsible for designing robust decision-making mechanisms for self-adaptive systems. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2211.17218v1-abstract-full').style.display = 'none'; document.getElementById('2211.17218v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 30 November, 2022; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> November 2022. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">24 pages</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2209.14041">arXiv:2209.14041</a> <span> [<a href="https://arxiv.org/pdf/2209.14041">pdf</a>, <a href="https://arxiv.org/format/2209.14041">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Robotics">cs.RO</span> </div> <div class="is-inline-block" style="margin-left: 0.5rem"> <div class="tags has-addons"> <span class="tag is-dark is-size-7">doi</span> <span class="tag is-light is-size-7"><a class="" href="https://doi.org/10.4204/EPTCS.371.12">10.4204/EPTCS.371.12 <i class="fa fa-external-link" aria-hidden="true"></i></a></span> </div> </div> </div> <p class="title is-5 mathjax"> Towards Adaptive Planning of Assistive-care Robot Tasks </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Hamilton%2C+J">Jordan Hamilton</a>, <a href="/search/cs?searchtype=author&query=Stefanakos%2C+I">Ioannis Stefanakos</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=C%C3%A1mara%2C+J">Javier C谩mara</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2209.14041v1-abstract-short" style="display: inline;"> This 'research preview' paper introduces an adaptive path planning framework for robotic mission execution in assistive-care applications. The framework provides a graph-based environment modelling approach, with dynamic path finding performed using Dijkstra's algorithm. A predictive module that uses probabilistic model checking is applied to estimate the human's movement through the environment… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2209.14041v1-abstract-full').style.display = 'inline'; document.getElementById('2209.14041v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2209.14041v1-abstract-full" style="display: none;"> This 'research preview' paper introduces an adaptive path planning framework for robotic mission execution in assistive-care applications. The framework provides a graph-based environment modelling approach, with dynamic path finding performed using Dijkstra's algorithm. A predictive module that uses probabilistic model checking is applied to estimate the human's movement through the environment, allowing run-time re-planning of the robot's path. We illustrate the use of the framework for a simulated assistive-care case study in which a mobile robot navigates through the environment and monitors an end user with mild physical or cognitive impairments. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2209.14041v1-abstract-full').style.display = 'none'; document.getElementById('2209.14041v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 28 September, 2022; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> September 2022. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">In Proceedings FMAS2022 ASYDE2022, arXiv:2209.13181</span> </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Journal ref:</span> EPTCS 371, 2022, pp. 175-183 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2209.14040">arXiv:2209.14040</a> <span> [<a href="https://arxiv.org/pdf/2209.14040">pdf</a>, <a href="https://arxiv.org/format/2209.14040">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Multiagent Systems">cs.MA</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Robotics">cs.RO</span> </div> <div class="is-inline-block" style="margin-left: 0.5rem"> <div class="tags has-addons"> <span class="tag is-dark is-size-7">doi</span> <span class="tag is-light is-size-7"><a class="" href="https://doi.org/10.4204/EPTCS.371.11">10.4204/EPTCS.371.11 <i class="fa fa-external-link" aria-hidden="true"></i></a></span> </div> </div> </div> <p class="title is-5 mathjax"> Scheduling of Missions with Constrained Tasks for Heterogeneous Robot Systems </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=V%C3%A1zquez%2C+G">Gricel V谩zquez</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=C%C3%A1mara%2C+J">Javier C谩mara</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2209.14040v1-abstract-short" style="display: inline;"> We present a formal tasK AllocatioN and scheduling apprOAch for multi-robot missions (KANOA). KANOA supports two important types of task constraints: task ordering, which requires the execution of several tasks in a specified order; and joint tasks, which indicates tasks that must be performed by more than one robot. To mitigate the complexity of robotic mission planning, KANOA handles the allocat… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2209.14040v1-abstract-full').style.display = 'inline'; document.getElementById('2209.14040v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2209.14040v1-abstract-full" style="display: none;"> We present a formal tasK AllocatioN and scheduling apprOAch for multi-robot missions (KANOA). KANOA supports two important types of task constraints: task ordering, which requires the execution of several tasks in a specified order; and joint tasks, which indicates tasks that must be performed by more than one robot. To mitigate the complexity of robotic mission planning, KANOA handles the allocation of the mission tasks to robots, and the scheduling of the allocated tasks separately. To that end, the task allocation problem is formalised in first-order logic and resolved using the Alloy model analyzer, and the task scheduling problem is encoded as a Markov decision process and resolved using the PRISM probabilistic model checker. We illustrate the application of KANOA through a case study in which a heterogeneous robotic team is assigned a hospital maintenance mission. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2209.14040v1-abstract-full').style.display = 'none'; document.getElementById('2209.14040v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 28 September, 2022; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> September 2022. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">In Proceedings FMAS2022 ASYDE2022, arXiv:2209.13181</span> </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">ACM Class:</span> I.2.11; D.4.1 </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Journal ref:</span> EPTCS 371, 2022, pp. 156-174 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2208.12723">arXiv:2208.12723</a> <span> [<a href="https://arxiv.org/pdf/2208.12723">pdf</a>, <a href="https://arxiv.org/format/2208.12723">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> </div> <p class="title is-5 mathjax"> Software Performability Analysis Using Fast Parametric Model Checking </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Fang%2C+X">Xinwei Fang</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Gerasimou%2C+S">Simos Gerasimou</a>, <a href="/search/cs?searchtype=author&query=Alhwikem%2C+F">Faisal Alhwikem</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2208.12723v2-abstract-short" style="display: inline;"> We present an efficient parametric model checking (PMC) technique for the analysis of software performability, i.e., of the performance and dependability properties of software systems. The new PMC technique works by automatically decomposing a parametric discrete-time Markov chain (pDTMC) model of the software system under verification into fragments that can be analysed independently, yielding r… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2208.12723v2-abstract-full').style.display = 'inline'; document.getElementById('2208.12723v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2208.12723v2-abstract-full" style="display: none;"> We present an efficient parametric model checking (PMC) technique for the analysis of software performability, i.e., of the performance and dependability properties of software systems. The new PMC technique works by automatically decomposing a parametric discrete-time Markov chain (pDTMC) model of the software system under verification into fragments that can be analysed independently, yielding results that are then combined to establish the required software performability properties. Our fast parametric model checking (fPMC) technique enables the formal analysis of software systems modelled by pDTMCs that are too complex to be handled by existing PMC methods. Furthermore, for many pDTMCs that state-of-the-art parametric model checkers can analyse, fPMC produces solutions (i.e., algebraic formulae) that are simpler and much faster to evaluate. We show experimentally that adding fPMC to the existing repertoire of PMC methods improves the efficiency of parametric model checking significantly, and extends its applicability to software systems with more complex behaviour than currently possible. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2208.12723v2-abstract-full').style.display = 'none'; document.getElementById('2208.12723v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 23 October, 2022; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 25 August, 2022; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> August 2022. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2205.03628">arXiv:2205.03628</a> <span> [<a href="https://arxiv.org/pdf/2205.03628">pdf</a>, <a href="https://arxiv.org/format/2205.03628">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> </div> <p class="title is-5 mathjax"> PRESTO: Predicting System-level Disruptions through Parametric Model Checking </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Fang%2C+X">Xinwei Fang</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Paterson%2C+C">Colin Paterson</a>, <a href="/search/cs?searchtype=author&query=Wilson%2C+J">Julie Wilson</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2205.03628v1-abstract-short" style="display: inline;"> Self-adaptive systems are expected to mitigate disruptions by continually adjusting their configuration and behaviour. This mitigation is often reactive. Typically, environmental or internal changes trigger a system response only after a violation of the system requirements. Despite a broad agreement that prevention is better than cure in self-adaptation, proactive adaptation methods are underrepr… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2205.03628v1-abstract-full').style.display = 'inline'; document.getElementById('2205.03628v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2205.03628v1-abstract-full" style="display: none;"> Self-adaptive systems are expected to mitigate disruptions by continually adjusting their configuration and behaviour. This mitigation is often reactive. Typically, environmental or internal changes trigger a system response only after a violation of the system requirements. Despite a broad agreement that prevention is better than cure in self-adaptation, proactive adaptation methods are underrepresented within the repertoire of solutions available to the developers of self-adaptive systems. To address this gap, we present a work-in-progress approach for the pre diction of system-level disruptions (PRESTO) through parametric model checking. Intended for use in the analysis step of the MAPE-K (Monitor-Analyse-Plan-Execute over a shared Knowledge) feedback control loop of self-adaptive systems, PRESTO comprises two stages. First, time-series analysis is applied to monitoring data in order to identify trends in the values of individual system and/or environment parameters. Next, future non-functional requirement violations are predicted by using parametric model checking, in order to establish the potential impact of these trends on the reliability and performance of the system. We illustrate the application of PRESTO in a case study from the autonomous farming domain. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2205.03628v1-abstract-full').style.display = 'none'; document.getElementById('2205.03628v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 7 May, 2022; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> May 2022. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">17th International Symposium on Software Engineering for Adaptive and Self-Managing Systems</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2202.03360">arXiv:2202.03360</a> <span> [<a href="https://arxiv.org/pdf/2202.03360">pdf</a>, <a href="https://arxiv.org/format/2202.03360">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> </div> </div> <p class="title is-5 mathjax"> Discrete-Event Controller Synthesis for Autonomous Systems with Deep-Learning Perception Components </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Imrie%2C+C">Calum Imrie</a>, <a href="/search/cs?searchtype=author&query=Mangal%2C+R">Ravi Mangal</a>, <a href="/search/cs?searchtype=author&query=Rodrigues%2C+G+N">Gena铆na Nunes Rodrigues</a>, <a href="/search/cs?searchtype=author&query=P%C4%83s%C4%83reanu%2C+C">Corina P膬s膬reanu</a>, <a href="/search/cs?searchtype=author&query=Santana%2C+M+A">Misael Alpizar Santana</a>, <a href="/search/cs?searchtype=author&query=V%C3%A1zquez%2C+G">Gricel V谩zquez</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2202.03360v2-abstract-short" style="display: inline;"> We present DeepDECS, a new method for the synthesis of correct-by-construction discrete-event controllers for autonomous systems that use deep neural network (DNN) classifiers for the perception step of their decision-making processes. Despite major advances in deep learning in recent years, providing safety guarantees for these systems remains very challenging. Our controller synthesis method add… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2202.03360v2-abstract-full').style.display = 'inline'; document.getElementById('2202.03360v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2202.03360v2-abstract-full" style="display: none;"> We present DeepDECS, a new method for the synthesis of correct-by-construction discrete-event controllers for autonomous systems that use deep neural network (DNN) classifiers for the perception step of their decision-making processes. Despite major advances in deep learning in recent years, providing safety guarantees for these systems remains very challenging. Our controller synthesis method addresses this challenge by integrating DNN verification with the synthesis of verified Markov models. The synthesised models correspond to discrete-event controllers guaranteed to satisfy the safety, dependability and performance requirements of the autonomous system, and to be Pareto optimal with respect to a set of optimisation objectives. We use the method in simulation to synthesise controllers for mobile-robot collision mitigation and for maintaining driver attentiveness in shared-control autonomous driving. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2202.03360v2-abstract-full').style.display = 'none'; document.getElementById('2202.03360v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 27 March, 2023; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 7 February, 2022; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> February 2022. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">18 pages 6 Figures 2 Tables</span> </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">ACM Class:</span> D.2.2; D.2.4; G.3; I.2.0; I.2.6 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2109.15139">arXiv:2109.15139</a> <span> [<a href="https://arxiv.org/pdf/2109.15139">pdf</a>, <a href="https://arxiv.org/format/2109.15139">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Distributed, Parallel, and Cluster Computing">cs.DC</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Networking and Internet Architecture">cs.NI</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Systems and Control">eess.SY</span> </div> <div class="is-inline-block" style="margin-left: 0.5rem"> <div class="tags has-addons"> <span class="tag is-dark is-size-7">doi</span> <span class="tag is-light is-size-7"><a class="" href="https://doi.org/10.1016/j.jss.2021.111208">10.1016/j.jss.2021.111208 <i class="fa fa-external-link" aria-hidden="true"></i></a></span> </div> </div> </div> <p class="title is-5 mathjax"> High-Availability Clusters: A Taxonomy, Survey, and Future Directions </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Somasekaram%2C+P">Premathas Somasekaram</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Buyya%2C+R">Rajkumar Buyya</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2109.15139v3-abstract-short" style="display: inline;"> The delivery of key services in domains ranging from finance and manufacturing to healthcare and transportation is underpinned by a rapidly growing number of mission-critical enterprise applications. Ensuring the continuity of these complex applications requires the use of software-managed infrastructures called high-availability clusters (HACs). HACs employ sophisticated techniques to monitor the… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2109.15139v3-abstract-full').style.display = 'inline'; document.getElementById('2109.15139v3-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2109.15139v3-abstract-full" style="display: none;"> The delivery of key services in domains ranging from finance and manufacturing to healthcare and transportation is underpinned by a rapidly growing number of mission-critical enterprise applications. Ensuring the continuity of these complex applications requires the use of software-managed infrastructures called high-availability clusters (HACs). HACs employ sophisticated techniques to monitor the health of key enterprise application layers and of the resources they use, and to seamlessly restart or relocate application components after failures. In this paper, we first describe the manifold uses of HACs to protect essential layers of a critical application and present the architecture of high availability clusters. We then propose a taxonomy that covers all key aspects of HACs -- deployment patterns, application areas, types of cluster, topology, cluster management, failure detection and recovery, consistency and integrity, and data synchronisation; and we use this taxonomy to provide a comprehensive survey of the end-to-end software solutions available for the HAC deployment of enterprise applications. Finally, we discuss the limitations and challenges of existing HAC solutions, and we identify opportunities for future research in the area. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2109.15139v3-abstract-full').style.display = 'none'; document.getElementById('2109.15139v3-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 21 September, 2022; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 30 September, 2021; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> September 2021. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Published in Journal of Systems and Software</span> </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Journal ref:</span> Journal of Systems and Software, Volume 187, 2022, 111208 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2109.02984">arXiv:2109.02984</a> <span> [<a href="https://arxiv.org/pdf/2109.02984">pdf</a>, <a href="https://arxiv.org/format/2109.02984">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> </div> <p class="title is-5 mathjax"> Quantitative Verification with Adaptive Uncertainty Reduction </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Alasmari%2C+N">Naif Alasmari</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Paterson%2C+C">Colin Paterson</a>, <a href="/search/cs?searchtype=author&query=Mirandola%2C+R">Raffaela Mirandola</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2109.02984v2-abstract-short" style="display: inline;"> Stochastic models are widely used to verify whether systems satisfy their reliability, performance and other nonfunctional requirements. However, the validity of the verification depends on how accurately the parameters of these models can be estimated using data from component unit testing, monitoring, system logs, etc. When insufficient data are available, the models are affected by epistemic pa… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2109.02984v2-abstract-full').style.display = 'inline'; document.getElementById('2109.02984v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2109.02984v2-abstract-full" style="display: none;"> Stochastic models are widely used to verify whether systems satisfy their reliability, performance and other nonfunctional requirements. However, the validity of the verification depends on how accurately the parameters of these models can be estimated using data from component unit testing, monitoring, system logs, etc. When insufficient data are available, the models are affected by epistemic parametric uncertainty, the verification results are inaccurate, and any engineering decisions based on them may be invalid. To address these problems, we introduce VERACITY, a tool-supported iterative approach for the efficient and accurate verification of nonfunctional requirements under epistemic parameter uncertainty. VERACITY integrates confidence-interval quantitative verification with a new adaptive uncertainty reduction heuristic that collects additional data about the parameters of the verified model by unit-testing specific system components over a series of verification iterations. VERACITY supports the quantitative verification of discrete-time Markov chains, deciding which components are to be tested in each iteration based on factors that include the sensitivity of the model to variations in the parameters of different components, and the overheads (e.g., time or cost) of unit-testing each of these components. We show the effectiveness and efficiency of VERACITY by using it for the verification of the nonfunctional requirements of a tele-assistance service-based system and an online shopping web application. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2109.02984v2-abstract-full').style.display = 'none'; document.getElementById('2109.02984v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 21 February, 2022; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 7 September, 2021; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> September 2021. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2106.06604">arXiv:2106.06604</a> <span> [<a href="https://arxiv.org/pdf/2106.06604">pdf</a>, <a href="https://arxiv.org/format/2106.06604">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Robotics">cs.RO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Human-Computer Interaction">cs.HC</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Systems and Control">eess.SY</span> </div> <div class="is-inline-block" style="margin-left: 0.5rem"> <div class="tags has-addons"> <span class="tag is-dark is-size-7">doi</span> <span class="tag is-light is-size-7"><a class="" href="https://doi.org/10.1016/j.scico.2022.102809">10.1016/j.scico.2022.102809 <i class="fa fa-external-link" aria-hidden="true"></i></a></span> </div> </div> </div> <p class="title is-5 mathjax"> Verified Synthesis of Optimal Safety Controllers for Human-Robot Collaboration </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Gleirscher%2C+M">Mario Gleirscher</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Douthwaite%2C+J">James Douthwaite</a>, <a href="/search/cs?searchtype=author&query=Lesage%2C+B">Benjamin Lesage</a>, <a href="/search/cs?searchtype=author&query=Paterson%2C+C">Colin Paterson</a>, <a href="/search/cs?searchtype=author&query=Aitken%2C+J">Jonathan Aitken</a>, <a href="/search/cs?searchtype=author&query=Alexander%2C+R">Rob Alexander</a>, <a href="/search/cs?searchtype=author&query=Law%2C+J">James Law</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2106.06604v1-abstract-short" style="display: inline;"> We present a tool-supported approach for the synthesis, verification and validation of the control software responsible for the safety of the human-robot interaction in manufacturing processes that use collaborative robots. In human-robot collaboration, software-based safety controllers are used to improve operational safety, e.g., by triggering shutdown mechanisms or emergency stops to avoid acci… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2106.06604v1-abstract-full').style.display = 'inline'; document.getElementById('2106.06604v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2106.06604v1-abstract-full" style="display: none;"> We present a tool-supported approach for the synthesis, verification and validation of the control software responsible for the safety of the human-robot interaction in manufacturing processes that use collaborative robots. In human-robot collaboration, software-based safety controllers are used to improve operational safety, e.g., by triggering shutdown mechanisms or emergency stops to avoid accidents. Complex robotic tasks and increasingly close human-robot interaction pose new challenges to controller developers and certification authorities. Key among these challenges is the need to assure the correctness of safety controllers under explicit (and preferably weak) assumptions. Our controller synthesis, verification and validation approach is informed by the process, risk analysis, and relevant safety regulations for the target application. Controllers are selected from a design space of feasible controllers according to a set of optimality criteria, are formally verified against correctness criteria, and are translated into executable code and validated in a digital twin. The resulting controller can detect the occurrence of hazards, move the process into a safe state, and, in certain circumstances, return the process to an operational state from which it can resume its original task. We show the effectiveness of our software engineering approach through a case study involving the development of a safety controller for a manufacturing work cell equipped with a collaborative robot. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2106.06604v1-abstract-full').style.display = 'none'; document.getElementById('2106.06604v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 11 June, 2021; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> June 2021. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">34 pages, 31 figures</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2103.02717">arXiv:2103.02717</a> <span> [<a href="https://arxiv.org/pdf/2103.02717">pdf</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> </div> <p class="title is-5 mathjax"> Uncertainty in Self-Adaptive Systems: A Research Community Perspective </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Hezavehi%2C+S+M">Sara M. Hezavehi</a>, <a href="/search/cs?searchtype=author&query=Weyns%2C+D">Danny Weyns</a>, <a href="/search/cs?searchtype=author&query=Avgeriou%2C+P">Paris Avgeriou</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Mirandola%2C+R">Raffaela Mirandola</a>, <a href="/search/cs?searchtype=author&query=Perez-Palacin%2C+D">Diego Perez-Palacin</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2103.02717v1-abstract-short" style="display: inline;"> One of the primary drivers for self-adaptation is ensuring that systems achieve their goals regardless of the uncertainties they face during operation. Nevertheless, the concept of uncertainty in self-adaptive systems is still insufficiently understood. Several taxonomies of uncertainty have been proposed, and a substantial body of work exists on methods to tame uncertainty. Yet, these taxonomies… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2103.02717v1-abstract-full').style.display = 'inline'; document.getElementById('2103.02717v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2103.02717v1-abstract-full" style="display: none;"> One of the primary drivers for self-adaptation is ensuring that systems achieve their goals regardless of the uncertainties they face during operation. Nevertheless, the concept of uncertainty in self-adaptive systems is still insufficiently understood. Several taxonomies of uncertainty have been proposed, and a substantial body of work exists on methods to tame uncertainty. Yet, these taxonomies and methods do not fully convey the research community's perception on what constitutes uncertainty in self-adaptive systems and how to tackle it. To understand this perception and learn from it, we conducted a survey comprising two complementary stages. In the first stage, we focused on current research and development. In the second stage, we focused on directions for future research. The key findings of the first stage are: a) an overview of uncertainty sources considered in self-adaptive systems, b) an overview of existing methods used to tackle uncertainty in concrete applications, c) insights into the impact of uncertainty on non-functional requirements, d) insights into different opinions in the perception of uncertainty within the community, and the need for standardised uncertainty-handling processes to facilitate uncertainty management in self-adaptive systems. The key findings of the second stage are: a) the insight that over 70% of the participants believe that self-adaptive systems can be engineered to cope with unanticipated change, b) a set of potential approaches for dealing with unanticipated change, c) a set of open challenges in mitigating uncertainty in self-adaptive systems, in particular in those with safety-critical requirements. From these findings, we outline an initial reference process to manage uncertainty in self-adaptive systems. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2103.02717v1-abstract-full').style.display = 'none'; document.getElementById('2103.02717v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 3 March, 2021; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> March 2021. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2103.01629">arXiv:2103.01629</a> <span> [<a href="https://arxiv.org/pdf/2103.01629">pdf</a>, <a href="https://arxiv.org/format/2103.01629">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> </div> </div> <p class="title is-5 mathjax"> DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Paterson%2C+C">Colin Paterson</a>, <a href="/search/cs?searchtype=author&query=Wu%2C+H">Haoze Wu</a>, <a href="/search/cs?searchtype=author&query=Grese%2C+J">John Grese</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Pasareanu%2C+C+S">Corina S. Pasareanu</a>, <a href="/search/cs?searchtype=author&query=Barrett%2C+C">Clark Barrett</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2103.01629v1-abstract-short" style="display: inline;"> We introduce DeepCert, a tool-supported method for verifying the robustness of deep neural network (DNN) image classifiers to contextually relevant perturbations such as blur, haze, and changes in image contrast. While the robustness of DNN classifiers has been the subject of intense research in recent years, the solutions delivered by this research focus on verifying DNN robustness to small pertu… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2103.01629v1-abstract-full').style.display = 'inline'; document.getElementById('2103.01629v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2103.01629v1-abstract-full" style="display: none;"> We introduce DeepCert, a tool-supported method for verifying the robustness of deep neural network (DNN) image classifiers to contextually relevant perturbations such as blur, haze, and changes in image contrast. While the robustness of DNN classifiers has been the subject of intense research in recent years, the solutions delivered by this research focus on verifying DNN robustness to small perturbations in the images being classified, with perturbation magnitude measured using established Lp norms. This is useful for identifying potential adversarial attacks on DNN image classifiers, but cannot verify DNN robustness to contextually relevant image perturbations, which are typically not small when expressed with Lp norms. DeepCert addresses this underexplored verification problem by supporting:(1) the encoding of real-world image perturbations; (2) the systematic evaluation of contextually relevant DNN robustness, using both testing and formal verification; (3) the generation of contextually relevant counterexamples; and, through these, (4) the selection of DNN image classifiers suitable for the operational context (i)envisaged when a potentially safety-critical system is designed, or (ii)observed by a deployed system. We demonstrate the effectiveness of DeepCert by showing how it can be used to verify the robustness of DNN image classifiers build for two benchmark datasets (`German Traffic Sign' and `CIFAR-10') to multiple contextually relevant perturbations. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2103.01629v1-abstract-full').style.display = 'none'; document.getElementById('2103.01629v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 2 March, 2021; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> March 2021. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2102.03298">arXiv:2102.03298</a> <span> [<a href="https://arxiv.org/pdf/2102.03298">pdf</a>, <a href="https://arxiv.org/format/2102.03298">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Robotics">cs.RO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Systems and Control">eess.SY</span> </div> <div class="is-inline-block" style="margin-left: 0.5rem"> <div class="tags has-addons"> <span class="tag is-dark is-size-7">doi</span> <span class="tag is-light is-size-7"><a class="" href="https://doi.org/10.1109/SEAMS51251.2021.00021">10.1109/SEAMS51251.2021.00021 <i class="fa fa-external-link" aria-hidden="true"></i></a></span> </div> </div> </div> <p class="title is-5 mathjax"> Maintaining driver attentiveness in shared-control autonomous driving </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Alasmari%2C+N">Naif Alasmari</a>, <a href="/search/cs?searchtype=author&query=Gleirscher%2C+M">Mario Gleirscher</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2102.03298v1-abstract-short" style="display: inline;"> We present a work-in-progress approach to improving driver attentiveness in cars provided with automated driving systems. The approach is based on a control loop that monitors the driver's biometrics (eye movement, heart rate, etc.) and the state of the car; analyses the driver's attentiveness level using a deep neural network; plans driver alerts and changes in the speed of the car using a formal… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2102.03298v1-abstract-full').style.display = 'inline'; document.getElementById('2102.03298v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2102.03298v1-abstract-full" style="display: none;"> We present a work-in-progress approach to improving driver attentiveness in cars provided with automated driving systems. The approach is based on a control loop that monitors the driver's biometrics (eye movement, heart rate, etc.) and the state of the car; analyses the driver's attentiveness level using a deep neural network; plans driver alerts and changes in the speed of the car using a formally verified controller; and executes this plan using actuators ranging from acoustic and visual to haptic devices. The paper presents (i) the self-adaptive system formed by this monitor-analyse-plan-execute (MAPE) control loop, the car and the monitored driver, and (ii) the use of probabilistic model checking to synthesise the controller for the planning step of the MAPE loop. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2102.03298v1-abstract-full').style.display = 'none'; document.getElementById('2102.03298v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 5 February, 2021; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> February 2021. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">7 pages, 6 figures</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2102.01564">arXiv:2102.01564</a> <span> [<a href="https://arxiv.org/pdf/2102.01564">pdf</a>, <a href="https://arxiv.org/format/2102.01564">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Artificial Intelligence">cs.AI</span> </div> </div> <p class="title is-5 mathjax"> Guidance on the Assurance of Machine Learning in Autonomous Systems (AMLAS) </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Hawkins%2C+R">Richard Hawkins</a>, <a href="/search/cs?searchtype=author&query=Paterson%2C+C">Colin Paterson</a>, <a href="/search/cs?searchtype=author&query=Picardi%2C+C">Chiara Picardi</a>, <a href="/search/cs?searchtype=author&query=Jia%2C+Y">Yan Jia</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Habli%2C+I">Ibrahim Habli</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2102.01564v1-abstract-short" style="display: inline;"> Machine Learning (ML) is now used in a range of systems with results that are reported to exceed, under certain conditions, human performance. Many of these systems, in domains such as healthcare , automotive and manufacturing, exhibit high degrees of autonomy and are safety critical. Establishing justified confidence in ML forms a core part of the safety case for these systems. In this document w… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2102.01564v1-abstract-full').style.display = 'inline'; document.getElementById('2102.01564v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2102.01564v1-abstract-full" style="display: none;"> Machine Learning (ML) is now used in a range of systems with results that are reported to exceed, under certain conditions, human performance. Many of these systems, in domains such as healthcare , automotive and manufacturing, exhibit high degrees of autonomy and are safety critical. Establishing justified confidence in ML forms a core part of the safety case for these systems. In this document we introduce a methodology for the Assurance of Machine Learning for use in Autonomous Systems (AMLAS). AMLAS comprises a set of safety case patterns and a process for (1) systematically integrating safety assurance into the development of ML components and (2) for generating the evidence base for explicitly justifying the acceptable safety of these components when integrated into autonomous system applications. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2102.01564v1-abstract-full').style.display = 'none'; document.getElementById('2102.01564v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 2 February, 2021; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> February 2021. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2102.01490">arXiv:2102.01490</a> <span> [<a href="https://arxiv.org/pdf/2102.01490">pdf</a>, <a href="https://arxiv.org/format/2102.01490">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Formal Languages and Automata Theory">cs.FL</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Robotics">cs.RO</span> </div> </div> <p class="title is-5 mathjax"> Fast Parametric Model Checking through Model Fragmentation </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Fang%2C+X">Xinwei Fang</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Gerasimou%2C+S">Simos Gerasimou</a>, <a href="/search/cs?searchtype=author&query=Alhwikem%2C+F">Faisal Alhwikem</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2102.01490v1-abstract-short" style="display: inline;"> Parametric model checking (PMC) computes algebraic formulae that express key non-functional properties of a system (reliability, performance, etc.) as rational functions of the system and environment parameters. In software engineering, PMC formulae can be used during design, e.g., to analyse the sensitivity of different system architectures to parametric variability, or to find optimal system con… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2102.01490v1-abstract-full').style.display = 'inline'; document.getElementById('2102.01490v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2102.01490v1-abstract-full" style="display: none;"> Parametric model checking (PMC) computes algebraic formulae that express key non-functional properties of a system (reliability, performance, etc.) as rational functions of the system and environment parameters. In software engineering, PMC formulae can be used during design, e.g., to analyse the sensitivity of different system architectures to parametric variability, or to find optimal system configurations. They can also be used at runtime, e.g., to check if non-functional requirements are still satisfied after environmental changes, or to select new configurations after such changes. However, current PMC techniques do not scale well to systems with complex behaviour and more than a few parameters. Our paper introduces a fast PMC (fPMC) approach that overcomes this limitation, extending the applicability of PMC to a broader class of systems than previously possible. To this end, fPMC partitions the Markov models that PMC operates with into \emph{fragments} whose reachability properties are analysed independently, and obtains PMC reachability formulae by combining the results of these fragment analyses. To demonstrate the effectiveness of fPMC, we show how our fPMC tool can analyse three systems (taken from the research literature, and belonging to different application domains) with which current PMC techniques and tools struggle. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2102.01490v1-abstract-full').style.display = 'none'; document.getElementById('2102.01490v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 2 February, 2021; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> February 2021. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2007.11099">arXiv:2007.11099</a> <span> [<a href="https://arxiv.org/pdf/2007.11099">pdf</a>, <a href="https://arxiv.org/format/2007.11099">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Robotics">cs.RO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Cryptography and Security">cs.CR</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> <div class="is-inline-block" style="margin-left: 0.5rem"> <div class="tags has-addons"> <span class="tag is-dark is-size-7">doi</span> <span class="tag is-light is-size-7"><a class="" href="https://doi.org/10.1007/978-3-030-78513-0_11">10.1007/978-3-030-78513-0_11 <i class="fa fa-external-link" aria-hidden="true"></i></a></span> </div> </div> </div> <p class="title is-5 mathjax"> Challenges in the Safety-Security Co-Assurance of Collaborative Industrial Robots </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Gleirscher%2C+M">Mario Gleirscher</a>, <a href="/search/cs?searchtype=author&query=Johnson%2C+N">Nikita Johnson</a>, <a href="/search/cs?searchtype=author&query=Karachristou%2C+P">Panayiotis Karachristou</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Law%2C+J">James Law</a>, <a href="/search/cs?searchtype=author&query=Clark%2C+J">John Clark</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2007.11099v1-abstract-short" style="display: inline;"> The coordinated assurance of interrelated critical properties, such as system safety and cyber-security, is one of the toughest challenges in critical systems engineering. In this chapter, we summarise approaches to the coordinated assurance of safety and security. Then, we highlight the state of the art and recent challenges in human-robot collaboration in manufacturing both from a safety and sec… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2007.11099v1-abstract-full').style.display = 'inline'; document.getElementById('2007.11099v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2007.11099v1-abstract-full" style="display: none;"> The coordinated assurance of interrelated critical properties, such as system safety and cyber-security, is one of the toughest challenges in critical systems engineering. In this chapter, we summarise approaches to the coordinated assurance of safety and security. Then, we highlight the state of the art and recent challenges in human-robot collaboration in manufacturing both from a safety and security perspective. We conclude with a list of procedural and technological issues to be tackled in the coordinated assurance of collaborative industrial robots. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2007.11099v1-abstract-full').style.display = 'none'; document.getElementById('2007.11099v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 17 July, 2020; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> July 2020. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">23 pages, 4 tables, 1 figure</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2007.03340">arXiv:2007.03340</a> <span> [<a href="https://arxiv.org/pdf/2007.03340">pdf</a>, <a href="https://arxiv.org/format/2007.03340">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Robotics">cs.RO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Systems and Control">eess.SY</span> </div> <div class="is-inline-block" style="margin-left: 0.5rem"> <div class="tags has-addons"> <span class="tag is-dark is-size-7">doi</span> <span class="tag is-light is-size-7"><a class="" href="https://doi.org/10.1109/ICECCS51672.2020.00017">10.1109/ICECCS51672.2020.00017 <i class="fa fa-external-link" aria-hidden="true"></i></a></span> </div> </div> </div> <p class="title is-5 mathjax"> Safety Controller Synthesis for Collaborative Robots </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Gleirscher%2C+M">Mario Gleirscher</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2007.03340v1-abstract-short" style="display: inline;"> In human-robot collaboration (HRC), software-based automatic safety controllers (ASCs) are used in various forms (e.g. shutdown mechanisms, emergency brakes, interlocks) to improve operational safety. Complex robotic tasks and increasingly close human-robot interaction pose new challenges to ASC developers and certification authorities. Key among these challenges is the need to assure the correctn… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2007.03340v1-abstract-full').style.display = 'inline'; document.getElementById('2007.03340v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2007.03340v1-abstract-full" style="display: none;"> In human-robot collaboration (HRC), software-based automatic safety controllers (ASCs) are used in various forms (e.g. shutdown mechanisms, emergency brakes, interlocks) to improve operational safety. Complex robotic tasks and increasingly close human-robot interaction pose new challenges to ASC developers and certification authorities. Key among these challenges is the need to assure the correctness of ASCs under reasonably weak assumptions. To address this need, we introduce and evaluate a tool-supported ASC synthesis method for HRC in manufacturing. Our ASC synthesis is: (i) informed by the manufacturing process, risk analysis, and regulations; (ii) formally verified against correctness criteria; and (iii) selected from a design space of feasible controllers according to a set of optimality criteria. The synthesised ASC can detect the occurrence of hazards, move the process into a safe state, and, in certain circumstances, return the process to an operational state from which it can resume its original task. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2007.03340v1-abstract-full').style.display = 'none'; document.getElementById('2007.03340v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 7 July, 2020; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> July 2020. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2006.09233">arXiv:2006.09233</a> <span> [<a href="https://arxiv.org/pdf/2006.09233">pdf</a>, <a href="https://arxiv.org/format/2006.09233">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Systems and Control">eess.SY</span> </div> <div class="is-inline-block" style="margin-left: 0.5rem"> <div class="tags has-addons"> <span class="tag is-dark is-size-7">doi</span> <span class="tag is-light is-size-7"><a class="" href="https://doi.org/10.1109/ICECCS51672.2020.00020">10.1109/ICECCS51672.2020.00020 <i class="fa fa-external-link" aria-hidden="true"></i></a></span> </div> </div> </div> <p class="title is-5 mathjax"> Towards Deductive Verification of Control Algorithms for Autonomous Marine Vehicles </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Foster%2C+S">Simon Foster</a>, <a href="/search/cs?searchtype=author&query=Gleirscher%2C+M">Mario Gleirscher</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2006.09233v1-abstract-short" style="display: inline;"> The use of autonomous vehicles in real-world applications is often precluded by the difficulty of providing safety guarantees for their complex controllers. The simulation-based testing of these controllers cannot deliver sufficient safety guarantees, and the use of formal verification is very challenging due to the hybrid nature of the autonomous vehicles. Our work-in-progress paper introduces a… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2006.09233v1-abstract-full').style.display = 'inline'; document.getElementById('2006.09233v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2006.09233v1-abstract-full" style="display: none;"> The use of autonomous vehicles in real-world applications is often precluded by the difficulty of providing safety guarantees for their complex controllers. The simulation-based testing of these controllers cannot deliver sufficient safety guarantees, and the use of formal verification is very challenging due to the hybrid nature of the autonomous vehicles. Our work-in-progress paper introduces a formal verification approach that addresses this challenge by integrating the numerical computation of such a system (in GNU/Octave) with its hybrid system verification by means of a proof assistant (Isabelle). To show the effectiveness of our approach, we use it to verify differential invariants of an Autonomous Marine Vehicle with a controller switching between multiple modes. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2006.09233v1-abstract-full').style.display = 'none'; document.getElementById('2006.09233v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 16 June, 2020; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> June 2020. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1911.12780">arXiv:1911.12780</a> <span> [<a href="https://arxiv.org/pdf/1911.12780">pdf</a>, <a href="https://arxiv.org/format/1911.12780">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Computer Vision and Pattern Recognition">cs.CV</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Machine Learning">stat.ML</span> </div> </div> <p class="title is-5 mathjax"> Detection and Mitigation of Rare Subclasses in Deep Neural Network Classifiers </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Paterson%2C+C">Colin Paterson</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Picardi%2C+C">Chiara Picardi</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1911.12780v2-abstract-short" style="display: inline;"> Regions of high-dimensional input spaces that are underrepresented in training datasets reduce machine-learnt classifier performance, and may lead to corner cases and unwanted bias for classifiers used in decision making systems. When these regions belong to otherwise well-represented classes, their presence and negative impact are very hard to identify. We propose an approach for the detection an… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1911.12780v2-abstract-full').style.display = 'inline'; document.getElementById('1911.12780v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1911.12780v2-abstract-full" style="display: none;"> Regions of high-dimensional input spaces that are underrepresented in training datasets reduce machine-learnt classifier performance, and may lead to corner cases and unwanted bias for classifiers used in decision making systems. When these regions belong to otherwise well-represented classes, their presence and negative impact are very hard to identify. We propose an approach for the detection and mitigation of such rare subclasses in deep neural network classifiers. The new approach is underpinned by an easy-to-compute commonality metric that supports the detection of rare subclasses, and comprises methods for reducing the impact of these subclasses during both model training and model exploitation. We demonstrate our approach using two well-known datasets, MNIST's handwritten digits and Kaggle's cats/dogs, identifying rare subclasses and producing models which compensate for subclass rarity. In addition we demonstrate how our run-time approach increases the ability of users to identify samples likely to be misclassified at run-time. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1911.12780v2-abstract-full').style.display = 'none'; document.getElementById('1911.12780v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 7 July, 2021; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 28 November, 2019; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> November 2019. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">8 pages, 7 Figures, 2 Tables</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1905.04223">arXiv:1905.04223</a> <span> [<a href="https://arxiv.org/pdf/1905.04223">pdf</a>, <a href="https://arxiv.org/ps/1905.04223">ps</a>, <a href="https://arxiv.org/format/1905.04223">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Machine Learning">stat.ML</span> </div> </div> <p class="title is-5 mathjax"> Assuring the Machine Learning Lifecycle: Desiderata, Methods, and Challenges </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Ashmore%2C+R">Rob Ashmore</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Paterson%2C+C">Colin Paterson</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1905.04223v1-abstract-short" style="display: inline;"> Machine learning has evolved into an enabling technology for a wide range of highly successful applications. The potential for this success to continue and accelerate has placed machine learning (ML) at the top of research, economic and political agendas. Such unprecedented interest is fuelled by a vision of ML applicability extending to healthcare, transportation, defence and other domains of gre… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1905.04223v1-abstract-full').style.display = 'inline'; document.getElementById('1905.04223v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1905.04223v1-abstract-full" style="display: none;"> Machine learning has evolved into an enabling technology for a wide range of highly successful applications. The potential for this success to continue and accelerate has placed machine learning (ML) at the top of research, economic and political agendas. Such unprecedented interest is fuelled by a vision of ML applicability extending to healthcare, transportation, defence and other domains of great societal importance. Achieving this vision requires the use of ML in safety-critical applications that demand levels of assurance beyond those needed for current ML applications. Our paper provides a comprehensive survey of the state-of-the-art in the assurance of ML, i.e. in the generation of evidence that ML is sufficiently safe for its intended use. The survey covers the methods capable of providing such evidence at different stages of the machine learning lifecycle, i.e. of the complex, iterative process that starts with the collection of the data used to train an ML component for a system, and ends with the deployment of that component within the system. The paper begins with a systematic presentation of the ML lifecycle and its stages. We then define assurance desiderata for each stage, review existing methods that contribute to achieving these desiderata, and identify open challenges that require further research. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1905.04223v1-abstract-full').style.display = 'none'; document.getElementById('1905.04223v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 10 May, 2019; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> May 2019. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1903.04771">arXiv:1903.04771</a> <span> [<a href="https://arxiv.org/pdf/1903.04771">pdf</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> </div> <p class="title is-5 mathjax"> Perpetual Assurances for Self-Adaptive Systems </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Weyns%2C+D">Danny Weyns</a>, <a href="/search/cs?searchtype=author&query=Bencomo%2C+N">Nelly Bencomo</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=C%C3%A1mara%2C+J">Javier C谩mara</a>, <a href="/search/cs?searchtype=author&query=Ghezzi%2C+C">Carlo Ghezzi</a>, <a href="/search/cs?searchtype=author&query=Grassi%2C+V">Vincenzo Grassi</a>, <a href="/search/cs?searchtype=author&query=Grunske%2C+L">Lars Grunske</a>, <a href="/search/cs?searchtype=author&query=Inverardi%2C+P">Paola Inverardi</a>, <a href="/search/cs?searchtype=author&query=J%C3%A9z%C3%A9quel%2C+J">Jean-Marc J茅z茅quel</a>, <a href="/search/cs?searchtype=author&query=Malek%2C+S">Sam Malek</a>, <a href="/search/cs?searchtype=author&query=Mirandola%2C+R">Raffaela Mirandola</a>, <a href="/search/cs?searchtype=author&query=Mori%2C+M">Marco Mori</a>, <a href="/search/cs?searchtype=author&query=Tamburrelli%2C+G">Giordano Tamburrelli</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1903.04771v1-abstract-short" style="display: inline;"> Providing assurances for self-adaptive systems is challenging. A primary underlying problem is uncertainty that may stem from a variety of different sources, ranging from incomplete knowledge to sensor noise and uncertain behavior of humans in the loop. Providing assurances that the self-adaptive system complies with its requirements calls for an enduring process spanning the whole lifetime of the… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1903.04771v1-abstract-full').style.display = 'inline'; document.getElementById('1903.04771v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1903.04771v1-abstract-full" style="display: none;"> Providing assurances for self-adaptive systems is challenging. A primary underlying problem is uncertainty that may stem from a variety of different sources, ranging from incomplete knowledge to sensor noise and uncertain behavior of humans in the loop. Providing assurances that the self-adaptive system complies with its requirements calls for an enduring process spanning the whole lifetime of the system. In this process, humans and the system jointly derive and integrate new evidence and arguments, which we coined perpetual assurances for self-adaptive systems. In this paper, we provide a background framework and the foundation for perpetual assurances for self-adaptive systems. We elaborate on the concrete challenges of offering perpetual assurances, requirements for solutions, realization techniques and mechanisms to make solutions suitable. We also present benchmark criteria to compare solutions. We then present a concrete exemplar that researchers can use to assess and compare approaches for perpetual assurances for self-adaptation. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1903.04771v1-abstract-full').style.display = 'none'; document.getElementById('1903.04771v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 12 March, 2019; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> March 2019. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Journal ref:</span> Software Engineering for Self-Adaptive Systems III. Assurances, 2017 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1812.09952">arXiv:1812.09952</a> <span> [<a href="https://arxiv.org/pdf/1812.09952">pdf</a>, <a href="https://arxiv.org/format/1812.09952">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> </div> <p class="title is-5 mathjax"> Efficient Parametric Model Checking Using Domain Knowledge </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Paterson%2C+C">Colin Paterson</a>, <a href="/search/cs?searchtype=author&query=Johnson%2C+K">Kenneth Johnson</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1812.09952v1-abstract-short" style="display: inline;"> We introduce an efficient parametric model checking (ePMC) method for the analysis of reliability, performance and other quality-of-service (QoS) properties of software systems. ePMC speeds up the analysis of parametric Markov chains modelling the behaviour of software by exploiting domain-specific modelling patterns for the software components. To this end, ePMC precomputes closed-form expression… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1812.09952v1-abstract-full').style.display = 'inline'; document.getElementById('1812.09952v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1812.09952v1-abstract-full" style="display: none;"> We introduce an efficient parametric model checking (ePMC) method for the analysis of reliability, performance and other quality-of-service (QoS) properties of software systems. ePMC speeds up the analysis of parametric Markov chains modelling the behaviour of software by exploiting domain-specific modelling patterns for the software components. To this end, ePMC precomputes closed-form expressions for key QoS properties of such patterns, and uses these expressions in the analysis of whole-system models. To evaluate ePMC, we show that its application to service-based systems and multi-tier software architectures reduces analysis time by several orders of magnitude compared to current parametric model checking methods. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1812.09952v1-abstract-full').style.display = 'none'; document.getElementById('1812.09952v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 24 December, 2018; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> December 2018. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">ACM Class:</span> D.2.19.c; D.2.4.e </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1805.09614">arXiv:1805.09614</a> <span> [<a href="https://arxiv.org/pdf/1805.09614">pdf</a>, <a href="https://arxiv.org/format/1805.09614">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> </div> <p class="title is-5 mathjax"> Observation-Enhanced QoS Analysis of Component-Based Systems </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Paterson%2C+C">Colin Paterson</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1805.09614v1-abstract-short" style="display: inline;"> We present a new method for the accurate analysis of the quality-of-service (QoS) properties of component-based systems. Our method takes as input a QoS property of interest and a high-level continuous-time Markov chain (CTMC) model of the analysed system, and refines this CTMC based on observations of the execution times of the system components. The refined CTMC can then be analysed with existin… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1805.09614v1-abstract-full').style.display = 'inline'; document.getElementById('1805.09614v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1805.09614v1-abstract-full" style="display: none;"> We present a new method for the accurate analysis of the quality-of-service (QoS) properties of component-based systems. Our method takes as input a QoS property of interest and a high-level continuous-time Markov chain (CTMC) model of the analysed system, and refines this CTMC based on observations of the execution times of the system components. The refined CTMC can then be analysed with existing probabilistic model checkers to accurately predict the value of the QoS property. The paper describes the theoretical foundation underlying this model refinement, the tool we developed to automate it, and two case studies that apply our QoS analysis method to a service-based system implemented using public web services and to an IT support system at a large university, respectively. Our experiments show that traditional CTMC-based QoS analysis can produce highly inaccurate results and may lead to invalid engineering and business decisions. In contrast, our new method reduced QoS analysis errors by 84.4-89.6% for the service-based system and by 94.7-97% for the IT support system, significantly lowering the risk of such invalid decisions. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1805.09614v1-abstract-full').style.display = 'none'; document.getElementById('1805.09614v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 24 May, 2018; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> May 2018. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">22 pages, 12 figures</span> </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">ACM Class:</span> D.2; D.2.2; D.2.4 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1703.06350">arXiv:1703.06350</a> <span> [<a href="https://arxiv.org/pdf/1703.06350">pdf</a>, <a href="https://arxiv.org/format/1703.06350">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> </div> <p class="title is-5 mathjax"> Engineering Trustworthy Self-Adaptive Software with Dynamic Assurance Cases </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Weyns%2C+D">Danny Weyns</a>, <a href="/search/cs?searchtype=author&query=Gerasimou%2C+S">Simos Gerasimou</a>, <a href="/search/cs?searchtype=author&query=Iftikhar%2C+M+U">M. Usman Iftikhar</a>, <a href="/search/cs?searchtype=author&query=Habli%2C+I">Ibrahim Habli</a>, <a href="/search/cs?searchtype=author&query=Kelly%2C+T">Tim Kelly</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1703.06350v2-abstract-short" style="display: inline;"> Building on concepts drawn from control theory, self-adaptive software handles environmental and internal uncertainties by dynamically adjusting its architecture and parameters in response to events such as workload changes and component failures. Self-adaptive software is increasingly expected to meet strict functional and non-functional requirements in applications from areas as diverse as manuf… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1703.06350v2-abstract-full').style.display = 'inline'; document.getElementById('1703.06350v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1703.06350v2-abstract-full" style="display: none;"> Building on concepts drawn from control theory, self-adaptive software handles environmental and internal uncertainties by dynamically adjusting its architecture and parameters in response to events such as workload changes and component failures. Self-adaptive software is increasingly expected to meet strict functional and non-functional requirements in applications from areas as diverse as manufacturing, healthcare and finance. To address this need, we introduce a methodology for the systematic ENgineering of TRUstworthy Self-adaptive sofTware (ENTRUST). ENTRUST uses a combination of (1) design-time and runtime modelling and verification, and (2) industry-adopted assurance processes to develop trustworthy self-adaptive software and assurance cases arguing the suitability of the software for its intended application. To evaluate the effectiveness of our methodology, we present a tool-supported instance of ENTRUST and its use to develop proof-of-concept self-adaptive software for embedded and service-based systems from the oceanic monitoring and e-finance domains, respectively. The experimental results show that ENTRUST can be used to engineer self-adaptive software systems in different application domains and to generate dynamic assurance cases for these systems. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1703.06350v2-abstract-full').style.display = 'none'; document.getElementById('1703.06350v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 22 November, 2018; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 18 March, 2017; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> March 2017. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">29 pages, 24 figures</span> </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">ACM Class:</span> D.2.11; D.2.18; D.2.4.e; D.2 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1109.3444">arXiv:1109.3444</a> <span> [<a href="https://arxiv.org/pdf/1109.3444">pdf</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Computers and Society">cs.CY</span> </div> </div> <p class="title is-5 mathjax"> Large-scale Complex IT Systems </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Sommerville%2C+I">Ian Sommerville</a>, <a href="/search/cs?searchtype=author&query=Cliff%2C+D">Dave Cliff</a>, <a href="/search/cs?searchtype=author&query=Calinescu%2C+R">Radu Calinescu</a>, <a href="/search/cs?searchtype=author&query=Keen%2C+J">Justin Keen</a>, <a href="/search/cs?searchtype=author&query=Kelly%2C+T">Tim Kelly</a>, <a href="/search/cs?searchtype=author&query=Kwiatkowska%2C+M">Marta Kwiatkowska</a>, <a href="/search/cs?searchtype=author&query=McDermid%2C+J">John McDermid</a>, <a href="/search/cs?searchtype=author&query=Paige%2C+R">Richard Paige</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1109.3444v1-abstract-short" style="display: inline;"> This paper explores the issues around the construction of large-scale complex systems which are built as 'systems of systems' and suggests that there are fundamental reasons, derived from the inherent complexity in these systems, why our current software engineering methods and techniques cannot be scaled up to cope with the engineering challenges of constructing such systems. It then goes on to p… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1109.3444v1-abstract-full').style.display = 'inline'; document.getElementById('1109.3444v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1109.3444v1-abstract-full" style="display: none;"> This paper explores the issues around the construction of large-scale complex systems which are built as 'systems of systems' and suggests that there are fundamental reasons, derived from the inherent complexity in these systems, why our current software engineering methods and techniques cannot be scaled up to cope with the engineering challenges of constructing such systems. It then goes on to propose a research and education agenda for software engineering that identifies the major challenges and issues in the development of large-scale complex, software-intensive systems. Central to this is the notion that we cannot separate software from the socio-technical environment in which it is used. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1109.3444v1-abstract-full').style.display = 'none'; document.getElementById('1109.3444v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 15 September, 2011; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> September 2011. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">12 pages, 2 figures</span> </p> </li> </ol> <div class="is-hidden-tablet">  <span class="help" style="display: inline-block;"><a href="https://github.com/arXiv/arxiv-search/releases">Search v0.5.6 released 2020-02-24</a>  </span> </div> </div> </main> <footer> <div class="columns is-desktop" role="navigation" aria-label="Secondary">  <div class="column"> <div class="columns"> <div class="column"> <ul class="nav-spaced"> <li><a href="https://info.arxiv.org/about">About</a></li> <li><a href="https://info.arxiv.org/help">Help</a></li> </ul> </div> <div class="column"> <ul class="nav-spaced"> <li> <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512" class="icon filter-black" role="presentation"><title>contact arXiv</title><desc>Click here to contact arXiv</desc><path d="M502.3 190.8c3.9-3.1 9.7-.2 9.7 4.7V400c0 26.5-21.5 48-48 48H48c-26.5 0-48-21.5-48-48V195.6c0-5 5.7-7.8 9.7-4.7 22.4 17.4 52.1 39.5 154.1 113.6 21.1 15.4 56.7 47.8 92.2 47.6 35.7.3 72-32.8 92.3-47.6 102-74.1 131.6-96.3 154-113.7zM256 320c23.2.4 56.6-29.2 73.4-41.4 132.7-96.3 142.8-104.7 173.4-128.7 5.8-4.5 9.2-11.5 9.2-18.9v-19c0-26.5-21.5-48-48-48H48C21.5 64 0 85.5 0 112v19c0 7.4 3.4 14.3 9.2 18.9 30.6 23.9 40.7 32.4 173.4 128.7 16.8 12.2 50.2 41.8 73.4 41.4z"/></svg> <a href="https://info.arxiv.org/help/contact.html"> Contact</a> </li> <li> <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512" class="icon filter-black" role="presentation"><title>subscribe to arXiv mailings</title><desc>Click here to subscribe</desc><path d="M476 3.2L12.5 270.6c-18.1 10.4-15.8 35.6 2.2 43.2L121 358.4l287.3-253.2c5.5-4.9 13.3 2.6 8.6 8.3L176 407v80.5c0 23.6 28.5 32.9 42.5 15.8L282 426l124.6 52.2c14.2 6 30.4-2.9 33-18.2l72-432C515 7.8 493.3-6.8 476 3.2z"/></svg> <a href="https://info.arxiv.org/help/subscribe"> Subscribe</a> </li> </ul> </div> </div> </div>   <div class="column"> <div class="columns"> <div class="column"> <ul class="nav-spaced"> <li><a href="https://info.arxiv.org/help/license/index.html">Copyright</a></li> <li><a href="https://info.arxiv.org/help/policies/privacy_policy.html">Privacy Policy</a></li> </ul> </div> <div class="column sorry-app-links"> <ul class="nav-spaced"> <li><a href="https://info.arxiv.org/help/web_accessibility.html">Web Accessibility Assistance</a></li> <li> <p class="help"> <a class="a11y-main-link" href="https://status.arxiv.org" target="_blank">arXiv Operational Status <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 256 512" class="icon filter-dark_grey" role="presentation"><path d="M224.3 273l-136 136c-9.4 9.4-24.6 9.4-33.9 0l-22.6-22.6c-9.4-9.4-9.4-24.6 0-33.9l96.4-96.4-96.4-96.4c-9.4-9.4-9.4-24.6 0-33.9L54.3 103c9.4-9.4 24.6-9.4 33.9 0l136 136c9.5 9.4 9.5 24.6.1 34z"/></svg></a><br> Get status notifications via <a class="is-link" href="https://subscribe.sorryapp.com/24846f03/email/new" target="_blank"><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512" class="icon filter-black" role="presentation"><path d="M502.3 190.8c3.9-3.1 9.7-.2 9.7 4.7V400c0 26.5-21.5 48-48 48H48c-26.5 0-48-21.5-48-48V195.6c0-5 5.7-7.8 9.7-4.7 22.4 17.4 52.1 39.5 154.1 113.6 21.1 15.4 56.7 47.8 92.2 47.6 35.7.3 72-32.8 92.3-47.6 102-74.1 131.6-96.3 154-113.7zM256 320c23.2.4 56.6-29.2 73.4-41.4 132.7-96.3 142.8-104.7 173.4-128.7 5.8-4.5 9.2-11.5 9.2-18.9v-19c0-26.5-21.5-48-48-48H48C21.5 64 0 85.5 0 112v19c0 7.4 3.4 14.3 9.2 18.9 30.6 23.9 40.7 32.4 173.4 128.7 16.8 12.2 50.2 41.8 73.4 41.4z"/></svg>email</a> or <a class="is-link" href="https://subscribe.sorryapp.com/24846f03/slack/new" target="_blank"><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 448 512" class="icon filter-black" role="presentation"><path d="M94.12 315.1c0 25.9-21.16 47.06-47.06 47.06S0 341 0 315.1c0-25.9 21.16-47.06 47.06-47.06h47.06v47.06zm23.72 0c0-25.9 21.16-47.06 47.06-47.06s47.06 21.16 47.06 47.06v117.84c0 25.9-21.16 47.06-47.06 47.06s-47.06-21.16-47.06-47.06V315.1zm47.06-188.98c-25.9 0-47.06-21.16-47.06-47.06S139 32 164.9 32s47.06 21.16 47.06 47.06v47.06H164.9zm0 23.72c25.9 0 47.06 21.16 47.06 47.06s-21.16 47.06-47.06 47.06H47.06C21.16 243.96 0 222.8 0 196.9s21.16-47.06 47.06-47.06H164.9zm188.98 47.06c0-25.9 21.16-47.06 47.06-47.06 25.9 0 47.06 21.16 47.06 47.06s-21.16 47.06-47.06 47.06h-47.06V196.9zm-23.72 0c0 25.9-21.16 47.06-47.06 47.06-25.9 0-47.06-21.16-47.06-47.06V79.06c0-25.9 21.16-47.06 47.06-47.06 25.9 0 47.06 21.16 47.06 47.06V196.9zM283.1 385.88c25.9 0 47.06 21.16 47.06 47.06 0 25.9-21.16 47.06-47.06 47.06-25.9 0-47.06-21.16-47.06-47.06v-47.06h47.06zm0-23.72c-25.9 0-47.06-21.16-47.06-47.06 0-25.9 21.16-47.06 47.06-47.06h117.84c25.9 0 47.06 21.16 47.06 47.06 0 25.9-21.16 47.06-47.06 47.06H283.1z"/></svg>slack</a> </p> </li> </ul> </div> </div> </div>  </div> </footer> <script src="https://static.arxiv.org/static/base/1.0.0a5/js/member_acknowledgement.js"></script> </body> </html>

CINXE.COM

Search | arXiv e-print repository