6 citations · 23 across the 11 of their papers we have counts for
12 papers
Deterministic Execution of ROS 2 Applications via Lingua Franca
Harun Teper, Shaokai Lin, Shulu Li +2
The Robot Operating System 2 (ROS 2) is a widely used middleware for robotic systems, characterized by a publish-subscribe (pub-sub) communication mechanism in which computation is…
Exploration of Approaches for Robustness and Safety in a Low Code Open Environment for Factory Automation
Gustavo Quiros A., Yi Peng Zhu, Tao Cui +3
This report is a compilation of technical knowledge and concepts that were produced by the authors and additional contributors in the context of the collaboration projects "Abstrac…
PolyVer: A Compositional Approach for Polyglot System Modeling and Verification
Pei-Wei Chen, Shaokai Lin, Adwait Godbole +4
Several software systems are polyglot; that is, they comprise programs implemented in a combination of programming languages. Verifiers that directly run on mainstream programming…
PretVM: Predictable, Efficient Virtual Machine for Real-Time Concurrency
Shaokai Lin, Erling Jellum, Mirco Theile +10
This paper introduces the Precision-Timed Virtual Machine (PretVM), an intermediate platform facilitating the execution of quasi-static schedules compiled from a subset of programs…
Strongly-Consistent Distributed Discrete-event Systems
Peter Donovan, Erling Jellum, Byeonggil Jun +5
Discrete-event (DE) systems are concurrent programs where components communicate via tagged events, where tags are drawn from a totally ordered set. Reactors are an emerging model…
Consistency vs. Availability in Distributed Real-Time Systems
Edward A. Lee, Ravi Akella, Soroush Bateni +3
In distributed applications, Brewer's CAP theorem tells us that when networks become partitioned (P), one must give up either consistency (C) or availability (A). Consistency is ag…
High-Performance Deterministic Concurrency using Lingua Franca
Christian Menard, Marten Lohstroh, Soroush Bateni +10
Actor frameworks and similar reactive programming techniques are widely used for building concurrent systems. They promise to be efficient and scale well to a large number of cores…
UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu +6
UCLID5 is a tool for the multi-modal formal modeling, verification, and synthesis of systems. It enables one to tackle verification problems for heterogeneous systems such as combi…
Xronos: Predictable Coordination for Safety-Critical Distributed Embedded Systems
Soroush Bateni, Marten Lohstroh, Hou Seng Wong +6
Asynchronous frameworks for distributed embedded systems, like ROS and MQTT, are increasingly used in safety-critical applications such as autonomous driving, where the cost of uni…
Quantifying and Generalizing the CAP Theorem
Edward A. Lee, Soroush Bateni, Shaokai Lin +2
In distributed applications, Brewer's CAP theorem tells us that when networks become partitioned, there is a tradeoff between consistency and availability. Consistency is agreement…
SciviK: A Versatile Framework for Specifying and Verifying Smart Contracts
Shaokai Lin, Xinyuan Sun, Jianan Yao +1
The growing adoption of smart contracts on blockchains poses new security risks that can lead to significant monetary loss, while existing approaches either provide no (or partial)…
Communication over Continuous Quantum Secure Dialogue using Einstein-Podolsky-Rosen States
Shaokai Lin, Zichuan Wang, Lior Horesh
With the emergence of quantum computing and quantum networks, many communication protocols that take advantage of the unique properties of quantum mechanics to achieve a secure bid…