Showing 1–24 of 24 results for author: Bensalem, S

Safeguarding Large Language Models: A Survey

Authors: Yi Dong, Ronghui Mu, Yanghao Zhang, Siqi Sun, Tianle Zhang, Changshun Wu, Gaojie **, Yi Qi, **wei Hu, Jie Meng, Saddek Bensalem, Xiaowei Huang

Abstract: In the burgeoning field of Large Language Models (LLMs), develo** a robust safety mechanism, colloquially known as "safeguards" or "guardrails", has become imperative to ensure the ethical use of LLMs within prescribed boundaries. This article provides a systematic literature review on the current status of this critical mechanism. It discusses its major challenges and how it can be enhanced int… ▽ More In the burgeoning field of Large Language Models (LLMs), develo** a robust safety mechanism, colloquially known as "safeguards" or "guardrails", has become imperative to ensure the ethical use of LLMs within prescribed boundaries. This article provides a systematic literature review on the current status of this critical mechanism. It discusses its major challenges and how it can be enhanced into a comprehensive mechanism dealing with ethical issues in various contexts. First, the paper elucidates the current landscape of safeguarding mechanisms that major LLM service providers and the open-source community employ. This is followed by the techniques to evaluate, analyze, and enhance some (un)desirable properties that a guardrail might want to enforce, such as hallucinations, fairness, privacy, and so on. Based on them, we review techniques to circumvent these controls (i.e., attacks), to defend the attacks, and to reinforce the guardrails. While the techniques mentioned above represent the current status and the active research trends, we also discuss several challenges that cannot be easily dealt with by the methods and present our vision on how to implement a comprehensive guardrail through the full consideration of multi-disciplinary approach, neural-symbolic method, and systems development lifecycle. △ Less

Submitted 3 June, 2024; originally announced June 2024.

Comments: under review. arXiv admin note: text overlap with arXiv:2402.01822

Formal Specification, Assessment, and Enforcement of Fairness for Generative AIs

Authors: Chih-Hong Cheng, Changshun Wu, Harald Ruess, Xingyu Zhao, Saddek Bensalem

Abstract: Reinforcing or even exacerbating societal biases and inequalities will increase significantly as generative AI increasingly produces useful artifacts, from text to images and beyond, for the real world. We address these issues by formally characterizing the notion of fairness for generative AI as a basis for monitoring and enforcing fairness. We define two levels of fairness using the notion of in… ▽ More Reinforcing or even exacerbating societal biases and inequalities will increase significantly as generative AI increasingly produces useful artifacts, from text to images and beyond, for the real world. We address these issues by formally characterizing the notion of fairness for generative AI as a basis for monitoring and enforcing fairness. We define two levels of fairness using the notion of infinite sequences of abstractions of AI-generated artifacts such as text or images. The first is the fairness demonstrated on the generated sequences, which is evaluated only on the outputs while agnostic to the prompts and models used. The second is the inherent fairness of the generative AI model, which requires that fairness be manifested when input prompts are neutral, that is, they do not explicitly instruct the generative AI to produce a particular type of output. We also study relative intersectional fairness to counteract the combinatorial explosion of fairness when considering multiple categories together with lazy fairness enforcement. Finally, fairness monitoring and enforcement are tested against some current generative AI models. △ Less

Submitted 6 May, 2024; v1 submitted 25 April, 2024; originally announced April 2024.

BAM: Box Abstraction Monitors for Real-time OoD Detection in Object Detection

Authors: Changshun Wu, Weicheng He, Chih-Hong Cheng, Xiaowei Huang, Saddek Bensalem

Abstract: Out-of-distribution (OoD) detection techniques for deep neural networks (DNNs) become crucial thanks to their filtering of abnormal inputs, especially when DNNs are used in safety-critical applications and interact with an open and dynamic environment. Nevertheless, integrating OoD detection into state-of-the-art (SOTA) object detection DNNs poses significant challenges, partly due to the complexi… ▽ More Out-of-distribution (OoD) detection techniques for deep neural networks (DNNs) become crucial thanks to their filtering of abnormal inputs, especially when DNNs are used in safety-critical applications and interact with an open and dynamic environment. Nevertheless, integrating OoD detection into state-of-the-art (SOTA) object detection DNNs poses significant challenges, partly due to the complexity introduced by the SOTA OoD construction methods, which require the modification of DNN architecture and the introduction of complex loss functions. This paper proposes a simple, yet surprisingly effective, method that requires neither retraining nor architectural change in object detection DNN, called Box Abstraction-based Monitors (BAM). The novelty of BAM stems from using a finite union of convex box abstractions to capture the learned features of objects for in-distribution (ID) data, and an important observation that features from OoD data are more likely to fall outside of these boxes. The union of convex regions within the feature space allows the formation of non-convex and interpretable decision boundaries, overcoming the limitations of VOS-like detectors without sacrificing real-time performance. Experiments integrating BAM into Faster R-CNN-based object detection DNNs demonstrate a considerably improved performance against SOTA OoD detection techniques. △ Less

Submitted 27 March, 2024; originally announced March 2024.

A Digital Twin prototype for traffic sign recognition of a learning-enabled autonomous vehicle

Authors: Mohamed AbdElSalam, Loai Ali, Saddek Bensalem, Weicheng He, Panagiotis Katsaros, Nikolaos Kekatos, Doron Peled, Anastasios Temperekidis, Changshun Wu

Abstract: In this paper, we present a novel digital twin prototype for a learning-enabled self-driving vehicle. The primary objective of this digital twin is to perform traffic sign recognition and lane kee**. The digital twin architecture relies on co-simulation and uses the Functional Mock-up Interface and SystemC Transaction Level Modeling standards. The digital twin consists of four clients, i) a vehi… ▽ More In this paper, we present a novel digital twin prototype for a learning-enabled self-driving vehicle. The primary objective of this digital twin is to perform traffic sign recognition and lane kee**. The digital twin architecture relies on co-simulation and uses the Functional Mock-up Interface and SystemC Transaction Level Modeling standards. The digital twin consists of four clients, i) a vehicle model that is designed in Amesim tool, ii) an environment model developed in Prescan, iii) a lane-kee** controller designed in Robot Operating System, and iv) a perception and speed control module developed in the formal modeling language of BIP (Behavior, Interaction, Priority). These clients interface with the digital twin platform, PAVE360-Veloce System Interconnect (PAVE360-VSI). PAVE360-VSI acts as the co-simulation orchestrator and is responsible for synchronization, interconnection, and data exchange through a server. The server establishes connections among the different clients and also ensures adherence to the Ethernet protocol. We conclude with illustrative digital twin simulations and recommendations for future work. △ Less

Submitted 14 February, 2024; originally announced February 2024.

What, Indeed, is an Achievable Provable Guarantee for Learning-Enabled Safety Critical Systems

Authors: Saddek Bensalem, Chih-Hong Cheng, Wei Huang, Xiaowei Huang, Changshun Wu, Xingyu Zhao

Abstract: Machine learning has made remarkable advancements, but confidently utilising learning-enabled components in safety-critical domains still poses challenges. Among the challenges, it is known that a rigorous, yet practical, way of achieving safety guarantees is one of the most prominent. In this paper, we first discuss the engineering and research challenges associated with the design and verificati… ▽ More Machine learning has made remarkable advancements, but confidently utilising learning-enabled components in safety-critical domains still poses challenges. Among the challenges, it is known that a rigorous, yet practical, way of achieving safety guarantees is one of the most prominent. In this paper, we first discuss the engineering and research challenges associated with the design and verification of such systems. Then, based on the observation that existing works cannot actually achieve provable guarantees, we promote a two-step verification method for the ultimate achievement of provable statistical guarantees. △ Less

Submitted 20 July, 2023; originally announced July 2023.

Towards Rigorous Design of OoD Detectors

Authors: Chih-Hong Cheng, Changshun Wu, Harald Ruess, Saddek Bensalem

Abstract: Out-of-distribution (OoD) detection techniques are instrumental for safety-related neural networks. We are arguing, however, that current performance-oriented OoD detection techniques geared towards matching metrics such as expected calibration error, are not sufficient for establishing safety claims. What is missing is a rigorous design approach for develo**, verifying, and validating OoD detec… ▽ More Out-of-distribution (OoD) detection techniques are instrumental for safety-related neural networks. We are arguing, however, that current performance-oriented OoD detection techniques geared towards matching metrics such as expected calibration error, are not sufficient for establishing safety claims. What is missing is a rigorous design approach for develo**, verifying, and validating OoD detectors. These design principles need to be aligned with the intended functionality and the operational domain. Here, we formulate some of the key technical challenges, together with a possible way forward, for develo** a rigorous and safety-related design methodology for OoD detectors. △ Less

Submitted 14 June, 2023; originally announced June 2023.

A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validation

Authors: Xiaowei Huang, Wenjie Ruan, Wei Huang, Gaojie **, Yi Dong, Changshun Wu, Saddek Bensalem, Ronghui Mu, Yi Qi, Xingyu Zhao, Kaiwen Cai, Yanghao Zhang, Sihao Wu, Peipei Xu, Dengyu Wu, Andre Freitas, Mustafa A. Mustafa

Abstract: Large Language Models (LLMs) have exploded a new heatwave of AI for their ability to engage end-users in human-level conversations with detailed and articulate answers across many knowledge domains. In response to their fast adoption in many industrial applications, this survey concerns their safety and trustworthiness. First, we review known vulnerabilities and limitations of the LLMs, categorisi… ▽ More Large Language Models (LLMs) have exploded a new heatwave of AI for their ability to engage end-users in human-level conversations with detailed and articulate answers across many knowledge domains. In response to their fast adoption in many industrial applications, this survey concerns their safety and trustworthiness. First, we review known vulnerabilities and limitations of the LLMs, categorising them into inherent issues, attacks, and unintended bugs. Then, we consider if and how the Verification and Validation (V&V) techniques, which have been widely developed for traditional software and deep learning models such as convolutional neural networks as independent processes to check the alignment of their implementations against the specifications, can be integrated and further extended throughout the lifecycle of the LLMs to provide rigorous analysis to the safety and trustworthiness of LLMs and their applications. Specifically, we consider four complementary techniques: falsification and evaluation, verification, runtime monitoring, and regulations and ethical use. In total, 370+ references are considered to support the quick understanding of the safety and trustworthiness issues from the perspective of V&V. While intensive research has been conducted to identify the safety and trustworthiness issues, rigorous yet practical methods are called for to ensure the alignment of LLMs with safety and trustworthiness requirements. △ Less

Submitted 27 August, 2023; v1 submitted 18 May, 2023; originally announced May 2023.

Prioritizing Corners in OoD Detectors via Symbolic String Manipulation

Authors: Chih-Hong Cheng, Changshun Wu, Emmanouil Seferis, Saddek Bensalem

Abstract: For safety assurance of deep neural networks (DNNs), out-of-distribution (OoD) monitoring techniques are essential as they filter spurious input that is distant from the training dataset. This paper studies the problem of systematically testing OoD monitors to avoid cases where an input data point is tested as in-distribution by the monitor, but the DNN produces spurious output predictions. We con… ▽ More For safety assurance of deep neural networks (DNNs), out-of-distribution (OoD) monitoring techniques are essential as they filter spurious input that is distant from the training dataset. This paper studies the problem of systematically testing OoD monitors to avoid cases where an input data point is tested as in-distribution by the monitor, but the DNN produces spurious output predictions. We consider the definition of "in-distribution" characterized in the feature space by a union of hyperrectangles learned from the training dataset. Thus the testing is reduced to finding corners in hyperrectangles distant from the available training data in the feature space. Concretely, we encode the abstract location of every data point as a finite-length binary string, and the union of all binary strings is stored compactly using binary decision diagrams (BDDs). We demonstrate how to use BDDs to symbolically extract corners distant from all data points within the training set. Apart from test case generation, we explain how to use the proposed corners to fine-tune the DNN to ensure that it does not predict overly confidently. The result is evaluated over examples such as number and traffic sign recognition. △ Less

Submitted 16 May, 2022; originally announced May 2022.

Customizable Reference Runtime Monitoring of Neural Networks using Resolution Boxes

Authors: Changshun Wu, Yliès Falcone, Saddek Bensalem

Abstract: Classification neural networks fail to detect inputs that do not fall inside the classes they have been trained for. Runtime monitoring techniques on the neuron activation pattern can be used to detect such inputs. We present an approach for monitoring classification systems via data abstraction. Data abstraction relies on the notion of box with a resolution. Box-based abstraction consists in repr… ▽ More Classification neural networks fail to detect inputs that do not fall inside the classes they have been trained for. Runtime monitoring techniques on the neuron activation pattern can be used to detect such inputs. We present an approach for monitoring classification systems via data abstraction. Data abstraction relies on the notion of box with a resolution. Box-based abstraction consists in representing a set of values by its minimal and maximal values in each dimension. We augment boxes with a notion of resolution and define their clustering coverage, which is intuitively a quantitative metric that indicates the abstraction quality. This allows studying the effect of different clustering parameters on the constructed boxes and estimating an interval of sub-optimal parameters. Moreover, we automatically construct monitors that leverage both the correct and incorrect behaviors of a system. This allows checking the size of the monitor abstractions and analyzing the separability of the network. Monitors are obtained by combining the sub-monitors of each class of the system placed at some selected layers. Our experiments demonstrate the effectiveness of our clustering coverage estimation and show how to assess the effectiveness and precision of monitors according to the selected clustering parameter and monitored layers. △ Less

Submitted 12 July, 2021; v1 submitted 25 April, 2021; originally announced April 2021.

Institution-based Encoding and Verification of Simple UML State Machines in CASL/SPASS

Authors: Tobias Rosenberger, Saddek Bensalem, Alexander Knapp, Markus Roggenbach

Abstract: This paper provides the first correct semantical representation of UML state-machines within the logical framework of an institution (previous attempts were flawed). A novel encoding of this representation into first-order logic enables symbolic analyses through a multitude of theorem-provers. UML state-machines are central to model-based systems-engineering. Till now, state-machine analysis has… ▽ More This paper provides the first correct semantical representation of UML state-machines within the logical framework of an institution (previous attempts were flawed). A novel encoding of this representation into first-order logic enables symbolic analyses through a multitude of theorem-provers. UML state-machines are central to model-based systems-engineering. Till now, state-machine analysis has been mostly restricted to model checking, which for state-machines suffers heavily from the state-space explosion problem. Symbolic reasoning, as enabled and demonstrated here, provides a powerful alternative, which can deal with large or even infinite state spaces. Full proofs are given. △ Less

Submitted 1 November, 2020; originally announced November 2020.

Performance Evaluation of the NDN Data Plane Using Statistical Model Checking

Authors: Siham Khoussi, Ayoub Nouri, Junxiao Shi, James Filliben, Lotfi Benmohamed, Abdella Battou, Saddek Bensalem

Abstract: Named Data Networking (NDN) is an emerging technology for a future internet architecture that addresses weaknesses of the Internet Protocol (IP). Since Internet users and applications have demonstrated an ever-increasing need for high speed packet forwarding, research groups have investigated different designs and implementation for fast NDN data plane forwarders and claimed they were capable of a… ▽ More Named Data Networking (NDN) is an emerging technology for a future internet architecture that addresses weaknesses of the Internet Protocol (IP). Since Internet users and applications have demonstrated an ever-increasing need for high speed packet forwarding, research groups have investigated different designs and implementation for fast NDN data plane forwarders and claimed they were capable of achieving high throughput rates. However, the correctness of these statements is not supported by any verification technique or formal proof. In this paper, we propose using a formal model-based approach to overcome this issue. We consider the NDN-DPDK prototype implementation of a forwarder realized at NIST, which leverages concurrency to enhance overall quality of service. We use our approach to improve its design and to formally show that it can achieve high throughput rates. △ Less

Submitted 26 July, 2019; v1 submitted 5 May, 2019; originally announced May 2019.

Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design

Authors: Simon Bliudze, Saddek Bensalem

Abstract: This volume contains the proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design (MeTRiD 2018), held on the 15th of April, 2018 in Thessaloniki, Greece as part of ETAPS 2018, the European Joint Conferences on Theory and Practice of Software. The term "Rigorous System Design" (RSD) denotes the design approach that is based on a formal, accountable and iterati… ▽ More This volume contains the proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design (MeTRiD 2018), held on the 15th of April, 2018 in Thessaloniki, Greece as part of ETAPS 2018, the European Joint Conferences on Theory and Practice of Software. The term "Rigorous System Design" (RSD) denotes the design approach that is based on a formal, accountable and iterative process for deriving trustworthy and optimised implementations from models of application software, its execution platform and its external environment. Ideally, a system implementation is derived from a set of appropriate high-level models by applying a sequence of semantics-preserving transformations. The ambition of MeTRiD is to promote the use of formal methods, in general, and the RSD approach, in particular, in the industrial applications and, reciprocally, bring the attention of the formal methods researchers to such industrial applications in order to develop realistic case-studies and guide the evolution of tools. Striving towards this ambitious goal, we have solicited contributions of three types: - regular papers, presenting original research - case study papers, reporting the evaluation of existing modelling, analysis, transformation and code generation formalisms and tools on realistic examples of significant size - tool papers, describing new tool prototypes supporting the RSD flow and enhancements of existing ones We have received 13 submissions (7 regular, 4 tool and 2 case study papers), whereof 8 have been accepted for presentation at the workshop: - 5 regular papers - 2 tool papers - 1 case study paper In this volume, these papers are complemented by an invited paper by Joseph Sifakis. △ Less

Submitted 25 June, 2018; originally announced June 2018.

Journal ref: EPTCS 272, 2018

Left-eigenvectors are certificates of the Orbit Problem

Authors: Steven de Oliveira, Virgile Prevosto, Peter Habermehl, Saddek Bensalem

Abstract: This paper investigates the connexion between the Kannan-Lipton Orbit Problem and the polynomial invariant generator algorithm PILA based on eigenvectors computation. Namely, we reduce the problem of generating linear and polynomial certificates of non-reachability for the Orbit Problem for linear transformations with rational coefficients to the generalized eigenvector problem. Also, we prove the… ▽ More This paper investigates the connexion between the Kannan-Lipton Orbit Problem and the polynomial invariant generator algorithm PILA based on eigenvectors computation. Namely, we reduce the problem of generating linear and polynomial certificates of non-reachability for the Orbit Problem for linear transformations with rational coefficients to the generalized eigenvector problem. Also, we prove the existence of such certificates for any transformation with integer coefficients, which is not the case with rational coefficients. △ Less

Submitted 26 March, 2018; originally announced March 2018.

Comments: 12 pages + references, submutted to ICALP 2018

Monitoring Distributed Component-Based Systems

Authors: Hosein Nazarpour, Yliès Falcone, Mohamad Jaber, Saddek Bensalem, Marius Bozga

Abstract: This paper addresses the online monitoring of distributed component-based systems with multi-party interactions against user-provided properties expressed in linear-temporal logic and referring to global states. We consider intrinsically independent components whose interactions are partitioned on distributed controllers. In this context, the problem that arises is that a global state of the syste… ▽ More This paper addresses the online monitoring of distributed component-based systems with multi-party interactions against user-provided properties expressed in linear-temporal logic and referring to global states. We consider intrinsically independent components whose interactions are partitioned on distributed controllers. In this context, the problem that arises is that a global state of the system is not available to the monitor. Instead, we attach local controllers to schedulers to retrieve the concurrent local traces. Local traces are sent to a global observer which reconstructs the set of global traces that are compatible with the local ones, in a concurrency-preserving fashion. In this context, the reconstruction of the global traces is done on-the-fly using a lattice of partial states encoding the global traces compatible with the locally-observed traces. We implemented our monitoring approach in a prototype tool called RVDIST. RVDIST executes in parallel with the distributed model and takes as input the events generated from each scheduler and outputs the evaluated computation lattice. Our experiments show that, thanks to the optimisation applied in the online monitoring algorithm, i) the size of the constructed computation lattice is insensitive to the the number of received events, (ii) the lattice size is kept reasonable and (iii) the overhead of the monitoring process is cheap. △ Less

Submitted 15 May, 2017; originally announced May 2017.

Concurrency-Preserving and Sound Monitoring of Multi-Threaded Component-Based Systems

Authors: Hosein Nazarpour, Yliès Falcone, Saddek Bensalem, Marius Bozga

Abstract: This paper addresses the monitoring of logic-independent linear-time user-provided properties in multi-threaded component-based systems. We consider intrinsically independent components that can be executed concurrently with a centralized coordination for multiparty interactions. In this context, the problem that arises is that a global state of the system is not available to the monitor. A naive… ▽ More This paper addresses the monitoring of logic-independent linear-time user-provided properties in multi-threaded component-based systems. We consider intrinsically independent components that can be executed concurrently with a centralized coordination for multiparty interactions. In this context, the problem that arises is that a global state of the system is not available to the monitor. A naive solution to this problem would be to plug in a monitor which would force the system to synchronize in order to obtain the sequence of global states at runtime. Such a solution would defeat the whole purpose of having concurrent components. Instead, we reconstruct on-the-fly the global states by accumulating the partial states traversed by the system at runtime. We define transformations of components that preserve their semantics and concurrency and, at the same time, allow to monitor global-state properties. Moreover, we present RVMT-BIP, a prototype tool implementing the transformations for monitoring multi-threaded systems described in the BIP (Behavior, Interaction, Priority) framework, an expressive framework for the formal construction of heterogeneous systems. Our experiments on several multi-threaded BIP systems show that RVMT-BIP induces a cheap runtime overhead. △ Less

Submitted 23 January, 2017; v1 submitted 19 December, 2016; originally announced December 2016.

Synthesizing invariants by solving solvable loops

Authors: Steven de Oliveira, Saddek Bensalem, Virgile Prevosto

Abstract: When proving invariance properties of a program, we face two problems. The first problem is related to the necessity of proving tautologies of considered assertion language, whereas the second manifests in the need of finding sufficiently strong invariants. This paper focuses on the second problem and describes a new method for the automatic generation of loop invariants that handles polynomial an… ▽ More When proving invariance properties of a program, we face two problems. The first problem is related to the necessity of proving tautologies of considered assertion language, whereas the second manifests in the need of finding sufficiently strong invariants. This paper focuses on the second problem and describes a new method for the automatic generation of loop invariants that handles polynomial and non deterministic assignments. This technique is based on the eigenvector generation for a given linear transformation and on the polynomial optimization problem, which we implemented in the open-source tool Pilat. △ Less

Submitted 23 November, 2016; originally announced November 2016.

Comments: 15 pages + 3 appendix

Polynomial invariants by linear algebra

Authors: Steven de Oliveira, Saddek Bensalem, Virgile Prevosto

Abstract: We present in this paper a new technique for generating polynomial invariants, divided in two independent parts : a procedure that reduces polynomial assignments composed loops analysis to linear loops under certain hypotheses and a procedure for generating inductive invariants for linear loops. Both of these techniques have a polynomial complexity for a bounded number of variables and we guarante… ▽ More We present in this paper a new technique for generating polynomial invariants, divided in two independent parts : a procedure that reduces polynomial assignments composed loops analysis to linear loops under certain hypotheses and a procedure for generating inductive invariants for linear loops. Both of these techniques have a polynomial complexity for a bounded number of variables and we guarantee the completeness of the technique for a bounded degree which we successfully implemented for C programs verification. △ Less

Submitted 23 November, 2016; originally announced November 2016.

Comments: 15 pages + 6 appendix

Journal ref: Automated Technology for Verification and Analysis 2016 Volume 9938 of the series Lecture Notes in Computer Science pp 479-494

Compositional Verification for Timed Systems Based on Automatic Invariant Generation

Authors: Lacramioara Astefanoaei, Souha Ben Rayana, Saddek Bensalem, Marius Bozga, Jacques Combaz

Abstract: We propose a method for compositional verification to address the state space explosion problem inherent to model-checking timed systems with a large number of components. The main challenge is to obtain pertinent global timing constraints from the timings in the components alone. To this end, we make use of auxiliary clocks to automatically generate new invariants which capture the constraints i… ▽ More We propose a method for compositional verification to address the state space explosion problem inherent to model-checking timed systems with a large number of components. The main challenge is to obtain pertinent global timing constraints from the timings in the components alone. To this end, we make use of auxiliary clocks to automatically generate new invariants which capture the constraints induced by the synchronisations between components. The method has been implemented in the RTD-Finder tool and successfully experimented on several benchmarks. △ Less

Submitted 16 September, 2015; v1 submitted 16 June, 2015; originally announced June 2015.

Journal ref: Logical Methods in Computer Science, Volume 11, Issue 3 (September 17, 2015) lmcs:1591

Timed Orchestration for Component-based Systems

Authors: Chih-Hong Cheng, Lacramioara Astefanoaei, Harald Ruess, Souha Ben Rayana, Saddek Bensalem

Abstract: Individual machines in flexible production lines explicitly expose capabilities at their interfaces by means of parametric skills. Given such a set of configurable machines, a line integrator is faced with the problem of finding and tuning parameters for each machine such that the overall production line implements given safety and temporal requirements in an optimized and robust fashion. We forma… ▽ More Individual machines in flexible production lines explicitly expose capabilities at their interfaces by means of parametric skills. Given such a set of configurable machines, a line integrator is faced with the problem of finding and tuning parameters for each machine such that the overall production line implements given safety and temporal requirements in an optimized and robust fashion. We formalize this problem of configuring and orchestrating flexible production lines as a parameter synthesis problem for systems of parametric timed automata, where interactions are based on skills. Parameter synthesis problems for interaction-level LTL properties are translated to parameter synthesis problems for state-based safety properties. For safety properties, synthesis problems are solved by checking satisfiability of $\exists\forall$SMT constraints. For constraint generation, we provide a set of computationally cheap over-approximations of the set of reachable states, together with fence constructions as sufficient conditions for safety formulas. We demonstrate the feasibility of our approach by solving typical machine configuration problems as encountered in industrial automation. △ Less

Submitted 20 May, 2016; v1 submitted 21 April, 2015; originally announced April 2015.

Comments: Timestamp of the work, with evaluation added by creating MES orchestration examples. (v3): typo fix and bring back definition and citation in en^t as in v1

A Verifiable and Correct-by-Construction Controller for Robot Functional Levels

Authors: Saddek Bensalem, Lavindra de Silva, Félix Ingrand, Rongjie Yan

Abstract: Autonomous robots are complex systems that require the interaction and cooperation between numerous heterogeneous software components. In recent times, robots are being increasingly used for complex and safety-critical tasks, such as exploring Mars and assisting/replacing humans. Consequently, robots are becoming critical systems that must meet safety properties, in particular, logical, temporal a… ▽ More Autonomous robots are complex systems that require the interaction and cooperation between numerous heterogeneous software components. In recent times, robots are being increasingly used for complex and safety-critical tasks, such as exploring Mars and assisting/replacing humans. Consequently, robots are becoming critical systems that must meet safety properties, in particular, logical, temporal and real-time constraints. To this end, we present an evolution of the LAAS architecture for autonomous systems, in particular its GenoM tool. This evolution relies on the BIP component-based design framework, which has been successfully used in other domains such as embedded systems. We show how we integrate BIP into our existing methodology for develo** the lowest (functional) level of robots. Particularly, we discuss the componentization of the functional level, the synthesis of an execution controller for it, and how we verify whether the resulting functional level conforms to properties such as deadlock-freedom. We also show through experimentation that the verification is feasible and usable for complex, real world robotic systems, and that the BIP-based functional levels resulting from our new methodology are, despite an overhead during execution, still practical on real world robotic platforms. Our approach has been fully implemented in the LAAS architecture, and the implementation has been used in several experiments on a real robot. △ Less

Submitted 2 September, 2013; originally announced September 2013.

Journal ref: Journal of Software Engineering for Robotics, 2(1), September 2011, pages 1-19

EFSMT: A Logical Framework for Cyber-Physical Systems

Authors: Chih-Hong Cheng, Natarajan Shankar, Harald Ruess, Saddek Bensalem

Abstract: The design of cyber-physical systems is challenging in that it includes the analysis and synthesis of distributed and embedded real-time systems for controlling, often in a nonlinear way, the environment. We address this challenge with EFSMT, the exists-forall quantified first-order fragment of propositional combinations over constraints (including nonlinear arithmetic), as the logical framework a… ▽ More The design of cyber-physical systems is challenging in that it includes the analysis and synthesis of distributed and embedded real-time systems for controlling, often in a nonlinear way, the environment. We address this challenge with EFSMT, the exists-forall quantified first-order fragment of propositional combinations over constraints (including nonlinear arithmetic), as the logical framework and foundation for analyzing and synthesizing cyber-physical systems. We demonstrate the expressiveness of EFSMT by reducing a number of pivotal verification and synthesis problems to EFSMT. Exemplary problems in this paper include synthesis for robust control via BIBO stability, Lyapunov coefficient finding for nonlinear control systems, distributed priority synthesis for orchestrating system components, and synthesis for hybrid control systems. We are also proposing an algorithm for solving EFSMT problems based on the interplay between two SMT solvers for respectively solving universally and existentially quantified problems. This algorithms builds on commonly used techniques in modern SMT solvers, and generalizes them to quantifier reasoning by counterexample-guided constraint strengthening. The EFSMT solver uses Bernstein polynomials for solving nonlinear arithmetic constraints. △ Less

Submitted 14 June, 2013; originally announced June 2013.

Distributed Priority Synthesis

Authors: Chih-Hong Cheng, Rongjie Yan, Saddek Bensalem, Harald Ruess

Abstract: Given a set of interacting components with non-deterministic variable update and given safety requirements, the goal of priority synthesis is to restrict, by means of priorities, the set of possible interactions in such a way as to guarantee the given safety conditions for all possible runs. In distributed priority synthesis we are interested in obtaining local sets of priorities, which are de… ▽ More Given a set of interacting components with non-deterministic variable update and given safety requirements, the goal of priority synthesis is to restrict, by means of priorities, the set of possible interactions in such a way as to guarantee the given safety conditions for all possible runs. In distributed priority synthesis we are interested in obtaining local sets of priorities, which are deployed in terms of local component controllers sharing intended next moves between components in local neighborhoods only. These possible communication paths between local controllers are specified by means of a communication architecture. We formally define the problem of distributed priority synthesis in terms of a multi-player safety game between players for (angelically) selecting the next transition of the components and an environment for (demonically) updating uncontrollable variables. We analyze the complexity of the problem, and propose several optimizations including a solution-space exploration based on a diagnosis method using a nested extension of the usual attractor computation in games together with a reduction to corresponding SAT problems. When diagnosis fails, the method proposes potential candidates to guide the exploration. These optimized algorithms for solving distributed priority synthesis problems have been integrated into the VissBIP framework. An experimental validation of this implementation is performed using a range of case studies including scheduling in multicore processors and modular robotics. △ Less

Submitted 26 November, 2012; originally announced November 2012.

Comments: In Proceedings SSV 2012, arXiv:1211.5873

Journal ref: EPTCS 102, 2012, pp. 57-72

Distributed Priority Synthesis and its Applications

Authors: Chih-Hong Cheng, Saddek Bensalem, Rongjie Yan, Harald Ruess, Christian Buckl, Alois Knoll

Abstract: Given a set of interacting components with non-deterministic variable update and given safety requirements, the goal of priority synthesis is to restrict, by means of priorities, the set of possible interactions in such a way as to guarantee the given safety conditions for all possible runs. In distributed priority synthesis we are interested in obtaining local sets of priorities, which are deploy… ▽ More Given a set of interacting components with non-deterministic variable update and given safety requirements, the goal of priority synthesis is to restrict, by means of priorities, the set of possible interactions in such a way as to guarantee the given safety conditions for all possible runs. In distributed priority synthesis we are interested in obtaining local sets of priorities, which are deployed in terms of local component controllers sharing intended next moves between components in local neighborhoods only. These possible communication paths between local controllers are specified by means of a communication architecture. We formally define the problem of distributed priority synthesis in terms of a multi-player safety game between players for (angelically) selecting the next transition of the components and an environment for (demonically) updating uncontrollable variables; this problem is NP-complete. We propose several optimizations including a solution-space exploration based on a diagnosis method using a nested extension of the usual attractor computation in games together with a reduction to corresponding SAT problems. When diagnosis fails, the method proposes potential candidates to guide the exploration. These optimized algorithms for solving distributed priority synthesis problems have been integrated into our VissBIP framework. An experimental validation of this implementation is performed using a range of case studies including scheduling in multicore processors and modular robotics. △ Less

Submitted 27 January, 2012; v1 submitted 8 December, 2011; originally announced December 2011.

Comments: 1. Timestamp the joint work "Distributed Priority Synthesis" from four institutes (Verimag, TUM, ISCAS, fortiss). 2. This version (v.2) updates related work in distributed synthesis

Algorithms for Synthesizing Priorities in Component-based Systems

Authors: Chih-Hong Cheng, Saddek Bensalem, Yu-Fang Chen, Rongjie Yan, Barbara Jobstmann, Harald Ruess, Christian Buckl, Alois Knoll

Abstract: We present algorithms to synthesize component-based systems that are safe and deadlock-free using priorities, which define stateless-precedence between enabled actions. Our core method combines the concept of fault-localization (using safety-game) and fault-repair (using SAT for conflict resolution). For complex systems, we propose three complementary methods as preprocessing steps for priority sy… ▽ More We present algorithms to synthesize component-based systems that are safe and deadlock-free using priorities, which define stateless-precedence between enabled actions. Our core method combines the concept of fault-localization (using safety-game) and fault-repair (using SAT for conflict resolution). For complex systems, we propose three complementary methods as preprocessing steps for priority synthesis, namely (a) data abstraction to reduce component complexities, (b) alphabet abstraction and #-deadlock to ignore components, and (c) automated assumption learning for compositional priority synthesis. △ Less

Submitted 7 October, 2011; v1 submitted 6 July, 2011; originally announced July 2011.

Comments: Full version of the ATVA'11 paper (compared to the 1st arXiv version, we add one additional sentence to avoid confusion)