Physical Sciences and Mathematics Commons^™

Formal Performance Guarantees For An Approach To Human In The Loop Robot Missions, Damian Lyons, Ron Arkin, Shu Jiang, Matt O'Brien, Feng Tang, Peng Tang

Faculty Publications

Abstract— A key challenge in the automatic verification of robot mission software, especially critical mission software, is to be able to effectively model the performance of a human operator and factor that into the formal performance guarantees for the mission. We present a novel approach to modelling the skill level of the operator and integrating it into automatic verification using a linear Gaussians model parameterized by experimental calibration. Our approach allows us to model different skill levels directly in terms of the behavior of the lumped, robot plus operator, system.

Using MissionLab and VIPARS (a behavior-based robot mission verification …

Performance Verification For Robot Missions In Uncertain Environments, Damian Lyons, Ron Arkin, Shu Jiang, Matt O'Brien, Feng Tang, Peng Tang

Faculty Publications

Abstract—Certain robot missions need to perform predictably in a physical environment that may have significant uncertainty. One approach is to leverage automatic software verification techniques to establish a performance guarantee. The addition of an environment model and uncertainty in both program and environment, however, means the state-space of a model-checking solution to the problem can be prohibitively large. An approach based on behavior-based controllers in a process-algebra framework that avoids state-space combinatorics is presented here. In this approach, verification of the robot program in the uncertain environment is reduced to a filtering problem for a Bayesian Network. Validation results …

Establishing A-Priori Performance Guarantees For Robot Missions That Include Localization Software, Damian Lyons, Ron Arkin, Shu Jiang, Matt O'Brien, Feng Tang, Peng Tang

Faculty Publications

One approach to determining whether an automated system is performing correctly is to monitor its performance, signaling when the performance is not acceptable; another approach is to automatically analyze the possible behaviors of the system a-priori and determine performance guarantees. Thea authors have applied this second approach to automatically derive performance guarantees for behaviorbased, multi-robot critical mission software using an innovative approach to formal verification for robotic software. Localization and mapping algorithms can allow a robot to navigate well in an unknown environment. However, whether such algorithms enhance any specific robot mission is currently a matter for empirical validation. Several …

Formal Performance Guarantees For Behavior-Based Localization Missions, Damian Lyons, Ron Arkin, Shu Jiang, Matt O'Brien, Feng Tang, Peng Tang

Faculty Publications

Abstract— Localization and mapping algorithms can allow a robot to navigate well in an unknown environment. However, whether such algorithms enhance any specific robot mission is currently a matter for empirical validation. In this paper we apply our MissionLab/VIPARS mission design and verification approach to an autonomous robot mission that uses probabilistic localization software.

Two approaches to modeling probabilistic localization for verification are presented: a high-level approach, and a sample-based approach which allows run-time code to be embedded in verification. Verification and experimental validation results are presented for two different missions, each using each method, demonstrating the accuracy …

Using Formal Methods To Verify Transactional Abstract Concurrency Control, Trek S. Palmer

Doctoral Dissertations

Concurrent application design and implementation is more important than ever in today's multi-core processor world. Transactional Memory (TM) Concurrent application design and implementation is more important than ever in today's multi-core processor world. Transactional Memory (TM). Each has its own particular advantages and disadvantages. However, these techniques each need some extra information to `glue' the non-transactional operation into a transactional context. At the most general level, non-transactional code must be decorated in such a way that the TM run-time can determine how those non-transactional operations commute with one another, and how to `undo' the non-transactional operations in case the run-time …

Probabilistic Verification Of Coordinated Multi-Robot Missions, Sagar J. Chaki, Joseph A. Giampapa

Joseph Andrew Giampapa

Robots are increasingly used to perform a wide variety of tasks, especially those involving dangerous or inaccessible locations. As the complexity of such tasks grow, robots are being deployed in teams, with complex coordination schemes aimed at maximizing the chance of mission success. Such teams operate under inherently uncertain conditions -- the robots themselves fail, and have to continuously adapt to changing environmental conditions. A key challenge facing robotic mission designers is therefore to construct a mission -- i.e., specify number and type of robots, number and size of teams, coordination and planning mechanisms etc. -- so as to maximize …

Getting It Right The First Time: Robot Mission Guarantees In The Presence Of Uncertainty, Damian Lyons, Ron Arkin, Paramesh Nirmal, Shu Jiang, Tsung-Ming Liu, Julia Deeb

Faculty Publications

Abstract—Certain robot missions need to perform predictably in a physical environment that may only be poorly characterized in advance. We have previously developed an approach to establishing performance guarantees for behavior-based controllers in a process-algebra framework. We extend that work here to include random variables, and we show how our prior results can be used to generate a Dynamic Bayesian Network for the coupled system of program and environment model. Verification is reduced to a filtering problem for this network. Finally, we present validation results that demonstrate the effectiveness of the verification of a multiple waypoint robot mission using this …

Program Analysis : Termination Proofs For Linear Simple Loops, Hongyi Chen

LSU Doctoral Dissertations

Termination proof synthesis for simple loops, i.e., loops with only conjoined constraints in the loop guard and variable updates in the loop body, is the building block of termination analysis, as well as liveness analysis, for large complex imperative systems. In particular, we consider a subclass of simple loops which contain only linear constraints in the loop guard and linear updates in the loop body. We call them Linear Simple Loops (LSLs). LSLs are particularly interesting because most loops in practice are indeed linear; more importantly, since we allow the update statements to handle nondeterminism, LSLs are expressive enough to …

Probabilistic Verification Of Coordinated Multi-Robot Missions, Sagar Chaki, Joseph Giampapa

Sagar J Chaki

Robots are increasingly used to perform a wide variety of tasks, especially those involving dangerous or inaccessible locations. As the complexity of such tasks grow, robots are being deployed in teams, with complex coordination schemes aimed at maximizing the chance of mission success. Such teams operate under inherently uncertain conditions -- the robots themselves fail, and have to continuously adapt to changing environmental conditions. A key challenge facing robotic mission designers is therefore to construct a mission -- i.e., specify number and type of robots, number and size of teams, coordination and planning mechanisms etc. -- so as to maximize …

Model Checking Software Architecture Design, Jiexin Zhang, Yang Liu, Jing Sun, Jin Song Dong, Jun Sun

Research Collection School Of Computing and Information Systems

Software Architecture plays an essential role in the high level description of a system design. Despite its importance in the software engineering practice, the lack of formal description and verification support hinders the development of quality architectural models. In this paper, we present an automated approach to the modeling and verification of software architecture designs using the Process Analysis Toolkit (PAT). We present the formal syntax of the Wright# architecture description language together with its operational semantics in Labeled Transition System (LTS). A dedicated model checking module for Wright# is implemented in the PAT verification framework based on the proposed …

Translating Pddl Into Csp# - The Pat Approach, Yi Li, Jing Sun, Jin Song Dong, Yang Liu, Jun Sun

Research Collection School Of Computing and Information Systems

Model checking provides a way to automatically verify hardware and software systems, whereas the goal of planning is to produce a sequence of actions that leads from the initial state to the desired goal state. Recently research indicates that there is a strong connection between model checking and planning problem solving. In this paper, we investigate the feasibility of using a newly developed model checking framework, Process Analysis Toolkit (PAT), to serve as a planning solution provider for upper layer applications. We first carried out a number of experiments on different planning tools in order to compare their performance and …

Deductive Formal Verification Of Embedded Systems, Zheng Lu

LSU Doctoral Dissertations

We combine static analysis techniques with model-based deductive verification using SMT solvers to provide a framework that, given an analysis aspect of the source code, automatically generates an analyzer capable of inferring information about that aspect.

The analyzer is generated by translating the collecting semantics of a program to a formula in first order logic over multiple underlying theories. We import the semantics of the API invocations as first order logic assertions. These assertions constitute the models used by the analyzer. Logical specification of the desired program behavior is incorporated as a first order logic formula. An SMT-LIB solver treats …

Unification Modulo Theories Of Blind Signatures, Serdar Erbatur

Legacy Theses & Dissertations (2009 - 2024)

This thesis is concerned with equational unification problems that are relevant in formal verification of cryptographic protocols which deploy blind signature schemes. Blind signatures are signature schemes that keep the content confidential and have applications in modern cryptography for electronic voting and digital cash schemes. Equational unification problems studied here originate from blind RSA signatures and El Gamal encryption.

Behavioral Signature-Based Framework For Identifying Unsatisfiable Variable Mappings Between Digital Designs, Vaibhav Uday Tendulkar

Browse all Theses and Dissertations

Throughout its design process (from specification to implementation) a digital circuit goes through a variety of structural changes. These changes are introduced primarily due to the use of automated tools in the design process. Checking whether the Boolean functions representing the two designs are equivalent is thus necessary to verify if a design implementation adheres to its specification. Combinational Equivalence Checking (CEC) - a process of determining whether two combinational design functions are equiv-alent, has been one of the most researched Boolean matching problems. The well-known CEC techniques that have been proposed adopt some kind of a formal approach such …

A Formal Framework For Modeling And Validating Simulink Diagrams, Chunqing Chen, Jin Song Dong, Jun Sun

Research Collection School Of Computing and Information Systems

Simulink has been widely used in industry to model and simulate embedded systems. With the increasing usage of embedded systems in real-time safety-critical situations, Simulink becomes deficient to analyze (timing) requirements with high-level assurance. In this article, we apply Timed Interval Calculus (TIC), a realtime specification language, to complement Simulink with TIC formal verification capability. We elaborately construct TIC library functions to model Simulink library blocks which are used to compose Simulink diagrams. Next, Simulink diagrams are automatically transformed into TIC models which preserve functional and timing aspects. Important requirements such as timing bounded liveness can be precisely specified in …

Machine-Assisted Proof Support For Validation Beyond Simulink, Chunqing Chen, Jin Song Dong, Jun Sun

Research Collection School Of Computing and Information Systems

Simulink is popular in industry for modeling and simulating embedded systems. It is deficient to handle requirements of high-level assurance and timing analysis. Previously, we showed the idea of applying Timed Interval Calculus (TIC) to complement Simulink. In this paper, we develop machine-assisted proof support for Simulink models represented in TIC. The work is based on a generic theorem prover, Prototype Verification System (PVS). The TIC specifications of both Simulink models and requirements are transformed to PVS specifications automatically. Verification can be carried out at interval level with a high level of automation. Analysis of continuous and discrete behaviors is …

Model Checking Control Communication Of A Facts Device, Bruce M. Mcmillin, J. K. Townsend, David Cape

Computer Science Faculty Research & Creative Works

This paper concerns the design and verification of a realtime communication protocol for sensor data collection and processing between an embedded computer and a DSP. In such systems, a certain amount of data loss without recovery may be tolerated. The key issue is to define and verify the correctness in the presence of these lost data frames under real-time constraints. This paper describes a temporal verification that if the end processes do not detect that too many frames are lost, defined by comparison of error counters against given threshold values, then there will be a bounded delay between transmission of …