Now showing items 1-6 of 6

A Semantic Framework for the Design of Distributed Reactive Real-Time Languages and Applications

Sanabria-Ardila, Mateo; Benavides-Navarro, Luis Daniel; Díaz-López, Daniel; Garzón-Alfonso, Wilmer (2020)

The proliferation of on-demand internet services delivered over a network of a heterogeneous set of computing devices has created the need for high-performing dynamic systems in real-time. Services such as audio and video ...
Reliable Control Architecture with PLEXIL and ROS for Autonomous Wheeled Robots

Cadavid, Héctor; Pérez, Alexander; Rocha, Camilo (Springer NatureSuiza, 2017)

Today’s autonomous robots are being used for complex tasks, including space exploration, military applications, and precision agriculture. As the complexity of control architectures increases, reliability of autonomous ...
Reliable Control Architecture with PLEXIL and ROS for Autonomous Wheeled Robots

Pérez, Alexander; Cadavid, Héctor; Rocha, Camilo (Springer NatureColombia, 2017)

Today’s autonomous robots are being used for complex tasks, including space exploration, military applications, and precision agriculture. As the complexity of control architectures increases, reliability of autonomous ...
Rewriting modulo SMT and open system analysis

Rocha, Camilo; Meseguer, José; Muñoz, César (Elsevier, 2016)

This paper proposes rewriting modulo SMT, a new technique that combines the power of SMT solving, rewriting modulo theories, and model checking. Rewriting modulo SMT is ideally suited to model and analyze reachability ...
Synchronous set relations in rewriting logic

Muñoz, César; Rocha Niño, Hernán Camilo (Elsevier, 2014)

This paper presents a mathematical foundation and a rewriting logic infrastructure for the execution and property verification of synchronous set relations. The mathematical foundation is given in the language of abstract ...
Towards Real-Time Semantics for a Distributed Event-Based MOP Language

Sanabria, Mateo; Garzón Alfonso, Wilmer; Benavides Navarro, Luis Daniel (Springer NatureSwitzerland., 2018)

This paper investigates rewriting logic as a suitable means to model the semantics of distributed and concurrent systems implemented using Monitoring Oriented Programming (MOP) frameworks. MOP tools close the gap between ...

Envíos recientes

A Semantic Framework for the Design of Distributed Reactive Real-Time Languages and Applications
...
Sanabria-Ardila, Mateo | 2020

The proliferation of on-demand internet services delivered over a network of a heterogeneous set of computing devices has created the need for high-performing dynamic systems in real-time. Services such as audio and video streaming, self-driving cars, the Internet of things (IoT), or instant communication on social networks have forced system designers to ethink the architectures and tools for implementing computer systems. Reactive programming has been advocated as a programming paradigm suitable for implementing dynamic applications with complex and heterogeneous architectural needs. However, there is no consensus on the core set of features that a reactive framework must-have. Furthermore, the current set of features proposed in reactive tools seems very restricted to cope with the actual needs for concurrency and distribution in modern systems. In this paper, several alternative semantics for distributed reactive languages are investigated, addressing complex open issues such as glitch avoidance, explicit distribution support, and constructs for explicit time management. First, we propose a reactive event-based programming language with explicit support for distribution, concurrency, and explicit time manipulation (ReactiveXD). Second, we present a reactive event-based semantic framework called Distributed Reactive Rewriting Framework (DRRF). The framework uses rewriting logic to model the components of a distributed base application, observables, and observers, and predicates supporting explicit time manipulation. Finally, to validate the proposal, the paper discusses the specification of the semantics of ReactiveXD and a scenario describing a case of intrusion detection on IoT networks

LEER
Reliable Control Architecture with PLEXIL and ROS for Autonomous Wheeled Robots
...
Cadavid, Héctor | 2017

Today’s autonomous robots are being used for complex tasks, including space exploration, military applications, and precision agriculture. As the complexity of control architectures increases, reliability of autonomous robots becomes more challenging to guarantee. This paper presents a hybrid control architecture, based on the Plan Execution Interchange Language ( PLEXIL ), for autonomy of wheeled robots running the Robot Operating System ( ROS ). PLEXIL is a synchronous reactive language developed by NASA for mission critical robotic systems, while ROS is one of the most popular frameworks for robotic middle-ware development. Given the safety-critical nature of spacecraft operations, PLEXIL operational semantics has been mathematically defined, and formal techniques and tools have been developed to automatically analyze plans written in this language. The hybrid control architecture proposed in this paper is showcased in a path tracking scenario using the Husky robot platform via a Gazebo simulation. Thanks to the architecture presented in this paper, all formal analysis techniques and tools currently available to PLEXIL are now available to build reliable plans for ROS -enabled wheeled robots.

LEER
Reliable Control Architecture with PLEXIL and ROS for Autonomous Wheeled Robots
...
Pérez, Alexander | 2017

Today’s autonomous robots are being used for complex tasks, including space exploration, military applications, and precision agriculture. As the complexity of control architectures increases, reliability of autonomous robots becomes more challenging to guarantee. This paper presents a hybrid control architecture, based on the Plan Execution Interchange Language ( PLEXIL ), for autonomy of wheeled robots running the Robot Operating System ( ROS ). PLEXIL is a synchronous reactive language developed by NASA for mission critical robotic systems, while ROS is one of the most popular frameworks for robotic middle-ware development. Given the safety-critical nature of spacecraft operations, PLEXIL operational semantics has been mathematically defined, and formal techniques and tools have been developed to automatically analyze plans written in this language. The hybrid control architecture proposed in this paper is showcased in a path tracking scenario using the Husky robot platform via a Gazebo simulation. Thanks to the architecture presented in this paper, all formal analysis techniques and tools currently available to PLEXIL are now available to build reliable plans for ROS -enabled wheeled robots.

LEER
Rewriting modulo SMT and open system analysis
...
Rocha, Camilo | 2016

This paper proposes rewriting modulo SMT, a new technique that combines the power of SMT solving, rewriting modulo theories, and model checking. Rewriting modulo SMT is ideally suited to model and analyze reachability properties of infinite-state open systems, i.e., systems that interact with a nondeterministic environment. Such systems exhibit both internal nondeterminism, which is proper to the system, and external nondeterminism, which is due to the environment. In a reflective formalism, such as rewriting logic, rewriting modulo SMT can be reduced to standard rewriting. Hence, rewriting modulo SMT naturally extends rewriting-based reachability analysis techniques, which are available for closed systems, to open systems. Furthermore, a single state expression with symbolic constraints can now denote an infinite set of concrete states. The proposed technique is illustrated with the formal analysis of: (i) a real-time system that is beyond the scope of timed-automata methods and (ii) automatic detection of reachability violations in a synchronous language developed to support autonomous spacecraft operations.

LEER
Synchronous set relations in rewriting logic
...
Muñoz, César | 2014

This paper presents a mathematical foundation and a rewriting logic infrastructure for the execution and property verification of synchronous set relations. The mathematical foundation is given in the language of abstract set relations. The infrastructure, which is written in the Maude system, enables the synchronous execution of a set relation provided by the user. By using the infrastructure, algorithm verification techniques such as reachability analysis and model checking, already available in Maude for traditional asynchronous rewriting, are automatically available to synchronous set rewriting. In this way, set-based synchronous languages and systems such as those built from agents, components, or objects can be naturally specified and simulated, and are also amenable to formal verification in the Maude system. The use of the infrastructure and some of its Maude-based verification capabilities are illustrated with an executable operational semantics of the Plan Execution Interchange Language (PLEXIL), a synchronous language developed by NASA to support autonomous spacecraft operations.

LEER
Towards Real-Time Semantics for a Distributed Event-Based MOP Language
...
Sanabria, Mateo | 2018

This paper investigates rewriting logic as a suitable means to model the semantics of distributed and concurrent systems implemented using Monitoring Oriented Programming (MOP) frameworks. MOP tools close the gap between specification and implementation, allowing several formal specifications and concrete implementations to be combined into a single executing system. To address real-time monitoring of modern distributed applications, we recently proposed REAL-T, a reactive event-based distributed programming language with explicit support for distributions and time manipulation. REAL-T allows programmers to instrument distributed applications to monitor and enforce specific behavior. It also supports requirements of modern reactive applications (responsiveness, resiliency, elasticity and asynchronous communication). The REAL-T programming model is very flexible, making the semantic specifications very challenging.

LEER

‹›

Repositorio Digital

Browsing by Subject "Rewriting logic"

A Semantic Framework for the Design of Distributed Reactive Real-Time Languages and Applications

Reliable Control Architecture with PLEXIL and ROS for Autonomous Wheeled Robots

Reliable Control Architecture with PLEXIL and ROS for Autonomous Wheeled Robots

Rewriting modulo SMT and open system analysis

Synchronous set relations in rewriting logic

Towards Real-Time Semantics for a Distributed Event-Based MOP Language

Envíos recientes

A Semantic Framework for the Design of Distributed Reactive Real-Time Languages and Applications

Reliable Control Architecture with PLEXIL and ROS for Autonomous Wheeled Robots

Reliable Control Architecture with PLEXIL and ROS for Autonomous Wheeled Robots

Rewriting modulo SMT and open system analysis

Synchronous set relations in rewriting logic

Towards Real-Time Semantics for a Distributed Event-Based MOP Language

Browsing by Subject "Rewriting logic"

A Semantic Framework for the Design of Distributed Reactive Real-Time Languages and Applications ﻿

Reliable Control Architecture with PLEXIL and ROS for Autonomous Wheeled Robots ﻿

Reliable Control Architecture with PLEXIL and ROS for Autonomous Wheeled Robots ﻿

Rewriting modulo SMT and open system analysis ﻿

Synchronous set relations in rewriting logic ﻿

Towards Real-Time Semantics for a Distributed Event-Based MOP Language ﻿

Envíos recientes

A Semantic Framework for the Design of Distributed Reactive Real-Time Languages and Applications

Reliable Control Architecture with PLEXIL and ROS for Autonomous Wheeled Robots

Reliable Control Architecture with PLEXIL and ROS for Autonomous Wheeled Robots

Rewriting modulo SMT and open system analysis

Synchronous set relations in rewriting logic

Towards Real-Time Semantics for a Distributed Event-Based MOP Language

A Semantic Framework for the Design of Distributed Reactive Real-Time Languages and Applications

Reliable Control Architecture with PLEXIL and ROS for Autonomous Wheeled Robots

Reliable Control Architecture with PLEXIL and ROS for Autonomous Wheeled Robots

Rewriting modulo SMT and open system analysis

Synchronous set relations in rewriting logic

Towards Real-Time Semantics for a Distributed Event-Based MOP Language