|
[RHO12]
Clinical Decision Support for Integrated Cyber-Physical Systems: A Mixed Methods Approach
Alex Roederer, Andrew Hicks, Enny Oyeniran, Insup Lee and Soojin Park
We describe the design and implementation of a clinical decision support system for assessing risk of cerebral vasospasm in patients who have been treated for aneurysmal subarachnoid hemorrhage. We illustrate the need for such clinical decision support systems in the intensive care environment, and propose a three pronged approach to constructing them, which we believe presents a balanced approach to patient modeling. We illustrate the data collection process, choice and development of models, system architecture, and methodology for user interface design. We close with a description of future work, a proposed evaluation mechanism, and a description of the demo to be presented.
[WJL09]
Formally Verifiable Networking
Anduo Wang, Limin Jia, Changbin Liu, Boon Thau Loo, Oleg Sokolsky, and Prithwish Basu
This paper proposes Formally Verifiable Networking (FVN), a novel approach towards unifying the design, specification, implementation, and verification of networking protocols within a logic-based framework. In FVN, formal logical statements are used to specify the behavior and the properties of the protocol. FVN uses declarative networking as an intermediary layer between high-level logical specifications of the network model and low-level implementations. A theorem prover is used to statically verify the properties of declarative network protocols. Moreover, a property preserving translation exists for generating declarative networking implementations from verified formal specifications. We further demonstrate the possibility of designing and specifying well-behaved network protocols with correctness guarantees in FVN using meta-models in a systematic and compositional way.
[WLL09]
A Theorem Proving Approach towards Declarative Networking
Anduo Wang, Boon Thau Loo, Changbin Liu, Oleg Sokolsky, and Prithwish Basu
We present the DRIVER system for designing, analyzing and implementing network protocols. DRIVER leverages declarative networking, a recent innovation that enables network protocols to be concisely specified and implemented using declarative languages. DRIVER takes as input declarative networking specifications written in the Network Datalog (NDlog) query language, and maps that automatically into logical specifications that can be directly used in existing theorem provers to validate protocol correctness. As an alternative approach, network designer can supply a component-based model of their routing design, automatically generate PVS specifications for verification and subsequent compilation into veriffied declarative network implementations. We demonstrate the use of DRIVER for synthesizing and verifying a variety of well-known network routing protocols.
[KPL12]
A Model-Based I/O Interface Synthesis Framework for the Cross-Platform Software Modeling
BaekGyu Kim, Linh T.X. Phan, Insup Lee, and Oleg Sokolsky
In model-based development, executable software (e.g., C or Java code) can be generated from a high-level model using a code generator. However, the execution of the generated software on a target platform remains a challenge due to a mismatch in communication semantics assumed by the model and the platform-dependent software (e.g., sampling/actuation routines). This paper proposes an input/output (I/O) interface module that bridges this semantic gap by means of buffers and interface policies, which explicitly capture the information required to adapt the model’s communication semantics to that of the platform. We present a framework that can be used to systematically synthesize – directly from the model – the I/O interfaces and accompanying APIs that the generated software and the platform-dependent software need to communicate with one another. Our interface policies can also encode relaxations of a model semantics that may not be implementable, thus making derivations of the implemented systems from the model traceable. We illustrate the applicability and the benefits of our framework with a case study of an infusion pump.
[ZSL09]
DMaC: Distributed Monitoring and Checking
Wenchao Zhou, Oleg Sokolsky, Boon Thau Loo, and Insup Lee
We consider monitoring and checking formally specified properties in a network. We are addressing the problem of deploying the checkers on different network nodes that provide correct and efficient checking. We present the DMaC system that builds upon two bodies of work: the Monitoring and Checking (MaC) framework, which provides means to monitor and check running systems against formally specified requirements, and declarative networking, a declarative domain-specific approach for specifying and implementing distributed network protocols. DMaC uses a declarative networking system for both specifying network protocols and performing checker execution. High-level properties are automatically translated from safety property specifications in the MaC framework into declarative networking queries and integrated into the rest of the network for monitoring the safety properties. We evaluate the flexibility and efficiency of DMaC using simple but realistic network protocols and their properties.
[WAS11]
Runtime Verification of Traces under Recording Uncertainty
Shaohui Wang, Anaheed Ayoub, Oleg Sokolsky, and Insup Lee
We present an on-line algorithm for the runtime checking of temporal properties, expressed as past-time Linear Temporal Logic (LTL) over the traces of observations recorded by a "black box"-like device. The recorder captures the observed values but not the precise time of their occurrences, and precise truth evaluation of a temporal logic formula cannot always be obtained. In order to handle this uncertainty, the checking algorithm is based on a three-valued semantics for pasttime LTL defined in this paper. In addition to the algorithm, the paper presents results of an evaluation that aimed to study the effects of the recording uncertainty on different kinds of temporal logic properties.
[PMS13]
Model-Driven Safety Analysis of Closed-Loop Medical Systems
Miroslav Pajic, Rahul Mangharam, Oleg Sokolsky, David Arney, Julian M. Goldman, and Insup Lee
In modern hospitals, patients are treated using a wide array of medical devices that are increasingly interacting with each other over the network, thus offering a perfect example of a cyber-physical system. We study the safety of a medical device system for the physiologic closed-loop control of drug infusion. The main contribution of the paper is the verification approach for the safety properties of closed-loop medical device systems. We demonstrate, using a case study, that the approach can be applied to a system of clinical importance. Our method combines simulation-based analysis of a detailed model of the system that contains continuous patient dynamics with model checking of a more abstract timed automata model. We show that the relationship between the two models preserves the crucial aspect of the timing behavior that ensures the conservativeness of the safety analysis. We also describe system design that can provide open-loop safety under network failure.
[CBC12]
Extending Task-level to Job-level Fixed Priority Assignment and Schedulability Analysis Using Pseudo-deadlines
Hoon Sung Chwa, Hyoungbu Back, Sanjian Chen, Jinkyu Lee, Arvind Easwaran, Insik Shin and Insup Lee
In global real-time multiprocessor scheduling, a
recent analysis technique for Task-level Fixed-Priority (TFP)
scheduling has been shown to outperform many of the analyses
for Job-level Fixed-Priority (JFP) scheduling on average. Since
JFP is a generalization of TFP scheduling, and the TFP analysis
technique itself has been adapted from an earlier JFP analysis,
this result is counter-intuitive and in our opinion highlights the
lack of good JFP scheduling techniques. Towards generalizing
the superior TFP analysis to JFP scheduling, we propose
the Smallest Pseudo-Deadline First (SPDF) JFP scheduling
algorithm. SPDF uses a simple task-level parameter called
pseudo-deadline to prioritize jobs, and hence can behave as a
TFP or JFP scheduler depending on the values of the pseudodeadlines.
This natural transition from TFP to JFP scheduling
has enabled us to incorporate the superior TFP analysis
technique in an SPDF schedulability test. We also present a
pseudo-deadline assignment algorithm for SPDF scheduling
that extends the well-known Optimal Priority Assignment
(OPA) algorithm for TFP scheduling. We show that our
algorithm is optimal for the derived schedulability test, and also
present a heuristic to overcome the computational complexity
issue of the optimal algorithm. Our simulation results show
that the SPDF algorithm with the new analysis significantly
outperforms state-of-the-art TFP and JFP analysis.
[KFS12]
Evaluation of a Smart Alarm for Intensive Care using Clinical Data
Andrew King, Kelsea Fortino, Nicholas Stevens, Sachin Shah, Margaret Fortino-Mullen and Insup Lee
We describe and report the results of an evaluation of a smart alarm algorithm for post coronary artery bypass graft (CABG) patients. The algorithm (CABG-SA) was applied to vital sign data streams recorded in a surgical intensive care unit (SICU) at a hospital in the University of Pennsylvania Health System. In order to determine the specificity of CABGSA, the alarms generated by CABG-SA were compared against the actual interventions performed by the staff of the critical care unit. Overall, CABG-SA alarmed for 55% of the time relative to traditional alarms while still generating alarms for 12 of the 13 recorded interventions.
[HKL12]
Rationale and Architecture Principles for Medical Application Platforms
John Hatcliff, Andrew King, Insup Lee, Alasdair MacDonald, Anura Fernando, Michael Robkin, Eugene Vasserman, Sandy Weininger and Julian Goldman
The concept of “system of systems” architecture is increasingly prevalent in many critical domains. Such systems allow information to be pulled from a variety of sources, analyzed to discover correlations and trends, stored to enable realtime and post-hoc assessment, mined to better inform decisionmaking, and leveraged to automate control of system units. In contrast, medical devices typically have been developed as monolithic stand-alone units. However, a vision is emerging of a notion of a medical application platform (MAP) that would provide device and health information systems (HIS) interoperability, safety critical network middleware, and an execution environment for clinical applications (“apps”) that offer numerous advantages for safety and effectiveness in health care delivery.
In this paper, we present the clinical safety/effectiveness and economic motivations for MAPs, and describe key characteristics of MAPs that are guiding the search for appropriate technology, regulatory, and ecosystem solutions. We give an overview of the Integrated Clinical Environment (ICE) – one particular achitecture for MAPs, and the Medical Device Coordination Framework – a prototype implementation of the ICE architecture.
[WCV12]
Trust in Collaborative Web Applications
Andrew West, Jian Chang, Krishna Venkatasubramanian, Insup Lee
Collaborative functionality is increasingly prevalent in web applications. Such functionality permits individuals to add - and sometimes modify - web content, often with minimal barriers to entry. Ideally, large bodies of knowledge can be amassed and shared in this manner. However, such software also provide a medium for nefarious persons to operate. By determining the extent to which participating content/agents can be trusted, one can identify useful contributions. In this work, we define the notion of trust for Collaborative Web Applications and survey the state-of-the-art for calculating, interpreting, and presenting trust values. Though techniques can be applied broadly, Wikipedia's archetypal nature makes it a focal point for discussion.
[NAV12]
Smart Alarms: Multivariate Medical Alarm Integration for post CABG surgery patients
Stevens Nicholas, Giannareas Ana, Kern Vanessa, Viesca Adrian, Fortino-Mullen Margaret, King Andrew, Lee Insup
In order to monitor patients in the Intensive Care Unit, healthcare practitioners set threshold alarms on each of many individual vital sign monitors. The current alarm algorithms elicit numerous false positive alarms producing an inefficient healthcare system, where nurses habitually ignore low level alarms due to their overabundance.
In this paper, we describe an algorithm that considers multiple vital signs when monitoring a post coronary artery bypass graft (post-CABG) surgery patient. The algorithm employs a Fuzzy Expert System to mimic the decision processes of nurses. In addition, it includes a Clinical Decision Support tool that uses Bayesian theory to display the possible CABG-related complications the patient might be undergoing at any point in time, as well as the most relevant risk factors. As a result, this multivariate approach decreases clinical alarms by an average of 59% with a standard deviation of 17% (Sample of 32 patients, 1,451 hours of vital sign data). Interviews comparing our proposed system with the approach currently used in hospitals have also confirmed the potential efficiency gains from this approach.
[SLH11]
Challenges in the Regulatory Approval of Medical Cyber-Physical Systems
Oleg Sokolsky, Insup Lee, and Mats Heimdahl
We are considering the challenges that regulators face in approving modern medical devices, which are software intensive and increasingly network enabled. We then consider assurance cases, which o er the means of organizing the evidence into a coherent argument demonstrating the level of assurance provided by a system, and discuss research directions that promise to make construction and evaluation of assurance cases easier and more precise. Finally, we discuss some recent trends that will further complicate the regulatory approval of medical cyber-physical systems.
[LSC12]
Challenges and Research Directions in Medical Cyber-Physical Systems
Insup Lee, Oleg Sokolsky, Sanjian Chen, John Hatcliff, Eunkyoung Jee, BaekGyu Kim, Andrew King, Margaret Mullen-Fortino, Soojin Park, Alexander Roederer, and Krishna Venkatasubramanian
Medical cyber-physical systems (MCPS) are lifecritical, context-aware, networked systems of medical devices. These systems are increasingly used in hospitals to provide highquality continuous care for patients. The need to design complex MCPS that are both safe and effective has presented numerous challenges, including achieving high assurance in system software, intoperability, context-aware intelligence, autonomy, security and privacy, and device certifiability. In this paper, we discuss these challenges in developing MCPS, some of our work in addressing them, and several open research issues.
[ACV12]
The Medical Device Dongle: An Open-Source Standards-Based Platform for Interoperable Medical Device Connectivity
Philip Asare, Danyang Cong, Santosh Vattam, Baek-Gyu Kim, Shan Lin, Oleg Sokolsky, Margaret Mullen-Fortino and Insup Lee
Emerging medical applications require device coordination, increasing the need to connect devices in an interoperable manner. However, many of the existing health devices in use were not originally developed for network connectivity and those devices with networking capabilities either use proprietary protocols or implementations of standard protocols that are unavailable to the end user. The first set of devices are unsuitable for device coordination applications and the second set are unsuitable for research in medical device interoperability. We propose the Medical Device Dongle (MDD), a low-cost, open-source platform that addresses both issues.
[AKL12]
A Safety Case Pattern for Model-Based Development Approach
Anaheed Ayoub, Baek-Gyu Kim, Insup Lee and Oleg Sokolsky
In this paper, a safety case pattern is introduced to facilitate the presentation of a correctness argument for a system implemented using formal methods in the development process. We took advantage of our experience in constructing a safety case for the Patient Controlled Analgesic (PCA) infusion pump, to define this safety case pattern. The proposed pattern is appropriate to be instantiated within the safety cases constructed for systems that are developed by applying model-based approaches.
[WHP12]
Spamming for Science: Active Measurement in Web 2.0 Abuse Research
Andrew West, Pedram Hayati, Vidyasagar Potdar, and Insup Lee
Spam and other electronic abuses have long been a focus of computer security research. However, recent work in the domain has emphasized an economic analysis of these operations in the hope of understanding and disrupting the profit model of attackers. Such studies do not lend themselves to passive measurement techniques. Instead, researchers have become middle-men or active participants in spam behaviors; methodologies that lie at an interesting juncture of legal, ethical, and human subject e.g., IRB) guidelines. In this work two such experiments serve as case studies: One testing a novel link spam model on Wikipedia and another using blackhat software to target blog comments and forums.
Discussion concentrates on the experimental design process, especially as in uenced by human-subject policy. Case studies are used to frame related work in the area, and scrutiny reveals the computer science community requires greater consistency in evaluating research of this nature.
[PLS12]
PADS: An approach to modeling resource demand and supply for the formal analysis of hierarchical scheduling
Anna Philippou, Insup Lee, and Oleg Sokolsky
As real-time embedded systems become more complex, resource partitioning is increasingly used to guarantee real-time performance. Recently, several compositional frameworks of resource partitioning have been proposed using real-time scheduling theory with various notions of real-time tasks running under restricted resource supply environments. However, these real-time scheduling-based approaches are limited in their expressiveness in that, although capable of describing resource-demand tasks, they are unable to model resource supply. This paper describes a process algebraic framework PADS for reasoning about resource demand and resource supply inspired by the timed process algebra ACSR. In ACSR, real-time tasks are specified by enunciating their consumption needs for resources. To also accommodate resource-supply processes in PADS, given a resource cpu we write c¯p¯u¯ to denote the availability of cpu for a requesting task process. Using PADS, we define a supply-demand relation where a pair (T , S) belongs to the relation if the demand process T can be scheduled under supply S. We develop a theory of compositional schedulability analysis as well as a technique for synthesizing an optimal supply process for a set of tasks. Furthermore, we define ordering relations between supplies which describe when a supply offers more resource capacity than another. With this notion it is possible to formally represent hierarchical scheduling approaches that assign more “generous” resource allocations to tasks in exchange for a simple representation. We illustrate our techniques via a number of examples.
[LXC12]
Realizing Compositional Scheduling through Virtualization
Jaewoo Lee, Sisu Xi, Sanjian Chen, Linh T.X. Phan, Chris Gill, Insup Lee, Chenyang Lu, Oleg Sokolsky
We present a co-designed scheduling framework and platform architecture that together support compositional scheduling of real-time systems. The architecture is built on the Xen virtualization platform, and relies on compositional scheduling theory that uses periodic resource models as component interfaces.We implement resource models as periodic servers and consider enhancements to periodic server design that significantly improve response times of tasks and resource utilization in the system while preserving theoretical schedulability results. We present an extensive evaluation of our implementation using workloads from an avionics case study as well as synthetic ones.
[PJL12]
From Verification to Implementation: A Model Translation Tool and a Pacemaker Case Study
Miroslav Pajic, Zhihao Jiang, Insup Lee, Oleg Sokolsky, and Rahul Mangharam
Model-Driven Design (MDD) of cyber-physical systems advocates for design procedures that start with formal modeling of the real-time system, followed by the model’s verification at an early stage. The verified model must then be translated to a more detailed model for simulation-based testing and finally translated into executable code in a physical implementation. As later stages build on the same core model, it is essential that models used earlier in the pipeline are valid approximations of the more detailed models developed downstream. The focus of this effort is on the design and development of a model translation tool, UPP2SF, and how it integrates system modeling, verification, model-based WCET analysis, simulation, code generation and testing into an MDD based framework. UPP2SF facilitates automatic conversion of verified timed automata-based models (in UPPAAL) to models that may be simulated and tested (in Simulink/Stateflow). We describe the design rules to ensure the conversion is correct, efficient and applicable to a large class of models. We show how the tool enables MDD of an implantable cardiac pacemaker. We demonstrate that UPP2SF preserves behaviors of the pacemaker model from UPPAAL to Stateflow. The resultant Stateflow chart is automatically converted into C and tested on a hardware platform for a set of requirements.
[CVW11]
AS-TRUST: A Trust Quantification Scheme for Autonomous Systems in BGP
Jian Chang, Krishna Venkatasubramanian, Andrew G. West, Sampath Kannan, Boon Thau Loo, Oleg Sokolsky, and Insup Lee
The Border Gateway Protocol (BGP) works by frequently exchanging updates that disseminate reachability information about IP prefixes (i.e., IP address blocks) between Autonomous Systems (ASes) on the Internet. The ideal operation of BGP relies on three major behavioral assumptions (BAs): (1) information contained in the update is legal and correct, (2) a route to a prefix is stable, and (3) the route adheres to the valley free routing policy. The current operation of BGP implicitly trusts all ASes to adhere to these assumptions. However, several documented violation of these assumptions attest to the fact that such an assumption of trust is perilous. This paper presents AS-TRUST, a scheme that comprehensively characterizes the trustworthiness of ASes with respect to their adherence of the behavioral assumptions. AS-TRUST quantifies trust using the notion of AS reputation. To compute reputation, AS-TRUST analyzes updates received in the past. It then classifies the resulting observations into multiple types of feedback. The feedback is used by a reputation function that uses Bayesian statistics to compute a probabilistic view of AS trustworthiness. This information can then be used for improving quotidian BGP operation by enabling improved route preference and dampening decision making at the ASes. Our implementation of AS-TRUST scheme using publicly available BGP traces demonstrates: (1) the number of ASes involved in violating the BGP behavioral assumptions is significant, and (2) the proposed reputation mechanism provides multi-fold improvement in the ability of ASes to operate in the presence of BA violations.
[JLS10]
Assurance Cases in Model-Driven Development of the Pacemaker Software
Eunkyoung Jee, Insup Lee and Oleg Sokolsky
We discuss the construction of an assurance case for the pace-maker software. The software is developed following a model-based technique that combined formal modeling of the system, systematic code generation from the formal model, and measurement of timing behavior of the implementation. We show how the structure of the assurance case reflects our development approach.
[WeLe11]
Multilingual Vandalism Detection using Language-Independent & Ex Post Facto Evidence
Andrew G. West and Insup Lee
There is much literature on Wikipedia vandalism detection. However, this writing addresses two facets given little treatment to date. First, prior efforts emphasize zero-delay detection, classifying edits the moment they are made. If classification can be delayed (e.g., compiling offline distributions), it is possible to leverage ex post facto evidence. This work describes/evaluates several features of this type, which we find to be overwhelmingly strong vandalism indicators.
Second, English Wikipedia has been the primary test-bed for research. Yet, Wikipedia has 200+ language editions and use of localized features impairs portability. This work implements an extensive set of language-independent indicators and evaluates them using three corpora (German, English, Spanish). The work then extends to include language-specific signals. Quantifying their performance benefit, we find that such features can moderately increase classifier accuracy, but significant effort and language fluency are required to capture this utility.
Aside from these novel aspects, this effort also broadly addresses the task, implementing 65 total features. Evaluation produces 0.840 PR-AUC on the zero-delay task and 0.906 PR-AUC with ex post facto evidence (averaging languages). Performance matches the state-of-the-art (English), sets novel baselines (German, Spanish), and is validated by a first-place finish over the 2011 PAN-CLEF test set.
[WeLe11]
Towards the Effective Temporal Association Mining of Spam Blacklists
Andrew G. West and Insup Lee
IP blacklists are a well-regarded anti-spam mechanism that capture global spamming patterns. These properties make such lists a practical ground-truth by which to study email spam behaviors. Observing one blacklist for nearly a year-and-a-half, we collected data on roughly *half a billion* listing events. In this paper, that data serves two purposes.
First, we conduct a measurement study on the dynamics of blacklists and email spam at-large. The magnitude/duration of the data enables scrutiny of long-term trends, at scale. Further, these statistics help parameterize our second task: the mining of blacklist history for temporal association rules. That is, we search for IP addresses with correlated histories. Strong correlations would suggest group members are not independent entities and likely share botnet membership.
Unfortunately, we find that statistically significant groupings are rare. This result is reinforced when rules are evaluated in terms of their ability to: (1) identify shared botnet members, using ground-truth from botnet infiltrations and sinkholes, and (2) predict future blacklisting events. In both cases, performance improvements over a control classifier are nominal. This outcome forces us to re-examine the appropriateness of blacklist data for this task, and suggest refinements to our mining model that may allow it to better capture the dynamics by which botnets operate.
[WCV11]
Link Spamming Wikipedia for Profit
Andrew G. West, Jian Chang, Krishna Venkatasubramanian, Oleg Sokolsky, and Insup Lee
Collaborative functionality is an increasingly prevalent web technology. To encourage participation, these systems usually have low barriers-to-entry and permissive privileges. Unsurprisingly, ill-intentioned users try to leverage these characteristics for nefarious purposes. In this work, a particular abuse is examined -- link spamming -- the addition of promotional or otherwise inappropriate hyperlinks.
Our analysis focuses on the "wiki" model and the collaborative encyclopedia, Wikipedia, in particular. A principal goal of spammers is to maximize *exposure*, the quantity of people who view a link. Creating and analyzing the first Wikipedia link spam corpus, we find that existing spam strategies perform quite poorly in this regard. The status quo spamming model relies on link persistence to accumulate exposures, a strategy that fails given the diligence of the Wikipedia community. Instead, we propose a model that exploits the latency inherent in human anti-spam enforcement.
Statistical estimation suggests our novel model would produce significantly more link exposures than status quo techniques. More critically, the strategy could prove economically viable for perpetrators, incentivizing its exploitation. To this end, we address mitigation strategies.
[WeLe11]
What Wikipedia Deletes: Characterizing Dangerous Collaborative Content
Andrew G. West and Insup Lee
Collaborative environments, such as Wikipedia, often have low barriers-to-entry in order to encourage participation. This accessibility is frequently abused (e.g., vandalism and spam). However, certain inappropriate behaviors are more threatening than others. In this work, we study contributions which are not simply ``undone'' -- but *deleted* from revision histories and public view. Such treatment is generally reserved for edits which: (1) present a legal liability to the host (e.g., copyright issues, defamation), or (2) present privacy threats to individuals (i.e., contact information).
Herein, we analyze one year of Wikipedia's public deletion log and use brute-force strategies to learn about privately handled redactions. This permits insight about the prevalence of deletion, the reasons that induce it, and the extent of end-user exposure to dangerous content. While Wikipedia's approach is generally quite reactive, we find that copyright issues prove most problematic of those behaviors studied.
[WAB11]
Autonomous Link Spam Detection in Purely Collaborative Environments
Andrew G. West, Avantika Agrawal, Phillip Baker, Brittney Exline, and Insup Lee
Collaborative models (e.g., wikis) are an increasingly prevalent Web technology. However, the open-access that defines such systems can also be utilized for nefarious purposes. In particular, this paper examines the use of collaborative functionality to add inappropriate hyperlinks to destinations outside the host environment (i.e., link spam). The collaborative encyclopedia, Wikipedia, is the basis for our analysis.
Recent research has exposed vulnerabilities in Wikipedia's link spam mitigation, finding that human editors are latent and dwindling in quantity. To this end, we propose and develop an autonomous classifier for link additions. Such a system presents unique challenges. For example, low barriers-to-entry invite a diversity of spam types, not just those with economic motivations. Moreover, issues can arise with how a link is presented (regardless of the destination).
In this work, a spam corpus is extracted from over 235,000 link additions to English Wikipedia. From this, 40+ features are codified and analyzed. These indicators are computed using "wiki" metadata, landing site analysis, and external data sources. The resulting classifier attains 64% recall at 0.5% false-positives (ROC-AUC=0.97). Such performance could enable egregious link additions to be blocked automatically with low false-positive rates, while prioritizing the remainder for human inspection. Finally, a live Wikipedia implementation of the technique has been developed.
[FTL09]
Hardware Acceleration for Conditional State-Based Communication
Scheduling on Real-Time Ethernet
Sebastian Fischmeister, Robert Trausmuth, and Insup Lee
Distributed real-time applications implement distributed applications with timeliness requirements. Such systems require a deterministic communication medium with bounded communication delays. Ethernet is a widely used commodity network with many appliances and network components and represents a natural fit for real-time application; unfortunately, standard Ethernet provides no bounded communication delays. Conditional state-based communication schedules provide expressive means for specifying and executing with choice points, while staying verifiable. Such schedules implement an arbitration scheme and provide the developer with means to fit the arbitration scheme to the application demands instead of requiring the developer to tweak the application to fit a predefined scheme. An evaluation of this approach as software prototypes showed that jitter and execution overhead may diminish the gains. This work successfully addresses this problem with a synthesized soft processor. We present results around the development of the soft processor, the design choices, and the measurements on throughput and robustness.
[CVW11]
ToMaTo: A Trustworthy Code Mashup Development Tool
Jian Chang, Krishna Venkatasubramanian, Andrew G. West, Sampath Kannan, Oleg Sokolsky, Myuhng Joo Kim, and Insup Lee
Recent years have seen the emergence of a new programming paradigm for Web applications that emphasizes the reuse of external content, the mashup. Although the mashup paradigm enables the creation of innovative Web applications with emergent features, its openness introduces trust problems. These trust issues are particularly prominent in JavaScript code mashup - a type of mashup that integrated external Javascript libraries to achieve function and software reuse. With JavaScript code mashup, external libraries are usually given full privileges to manipulate data of the mashup application and executing arbitrary code. This imposes considerable risk on the mashup developers and the end users.
One major causes for these trust problems is that the mashup developers tend to focus on the functional aspects of the application and implicitly trust the external code libraries to satisfy security, privacy and other non-functional requirements. In this paper, we present ToMaTo, a development tool that combines a novel trust policy language and a static code analysis engine to examine whether the external libraries satisfy the non-functional requirements. ToMaTo gives the mashup developers three essential capabilities for building trustworthy JavaScript code mashup: (1) to specify trust policy, (2) to assess policy adherence, and (3) to handle policy violation. The contributions of the paper are: (1) a description of JavaScript code mashup and its trust issues, and (2) a development tool (ToMaTo) for building trustworthy JavaScript code mashup.
[PLS11]
Compositional Analysis of Real-Time Embedded Systems
Linh T.X. Phan, Insup Lee, and Oleg Sokolsky
This tutorial is concerned with various aspects of component-based design and compositional analysis of real-time embedded systems. It will first give an overview of component-based frameworks and their underlying principles. It will then go in-depth into abstraction methods for real-time components and techniques for computing their optimal interfaces, for both systems implemented on uniprocessor and multiprocessor platforms, as well as extensions to multi-mode systems. Besides theoretical aspects, the tutorial will also present an implementation of the compositional analysis framework on Xen virtualization and a demonstration of the CARTS toolset with several examples seeing the techniques in action. It will also include two case studies highlighting the utility of the framework, including the ARINC-653 avionics software and a smart-phone application. We will conclude the tutorial with a number of open challenges and research opportunities in this domain.
[PhLe11]
Towards A Compositional Multi-Modal Framework for Adaptive Cyber-Physical Systems
Linh T. X. Phan and Insup Lee
Among the key characteristics of cyber-physical
systems are the ability to adapt to changes during operation,
the multidimensional complexity of multi-functionality and the
underlying heterogeneous distributed architecture, as well as
resource use efficiency. In this paper, we propose a compositional
multi-modal approach to modeling, analyzing, and designing such
systems. We introduce a general framework for modeling and
compositional analysis of multi-mode systems on a distributed
architecture that facilitates adaptivity, efficient use of resources,
and incremental integration. We present some preliminary results,
and we describe some of the remaining challenges and
future directions.
[GPC11]
Video Quality Driven Buffer Sizing via Frame Drops
Deepak Gangadharan, Linh T.X. Phan, Samarjit Chakraborty, Roger Zimmermann, and Insup Lee
We study the impact of video frame drops in buffer constrained
multiprocessor system-on-chip (MPSoC) platforms.
Since on-chip buffer memory occupies a significant amount of
silicon area, accurate buffer sizing has attracted a lot of research
interest lately. However, all previous work studied this problem
with the underlying assumption that no video frame drops
can be tolerated. In reality, multimedia applications can often
tolerate some frame drops without significantly deteriorating
their output quality. Although system simulations can be used
to perform video quality driven buffer sizing, they are time
consuming. In this paper, we first demonstrate a dual-buffer
management scheme to drop only the less significant frames.
Based on this scheme, we then propose a formal framework
to evaluate the buffer size vs. video quality trade-offs, which
in turn will help a system designer to perform quality driven
buffer sizing. In particular, we mathematically characterize the
maximum numbers of frame drops for various buffer sizes and
evaluate how they affect the worst-case PSNR value of the
decoded video. We evaluate our proposed framework with an
MPEG-2 decoder and compare the obtained results with that
of a cycle-accurate simulator. Our evaluations show that for an
acceptable quality of 30 dB, it is possible to reduce the buffer
size by upto 28.6% which amounts to 25.88 megabits.
[KAS11]
Safety-Assured Development of the GPCA Infusion Pump Software
BaekGyu Kim, Anaheed Ayoub, Oleg Sokolsky, Insup Lee, Paul Jones, Yi Zhang, and Raoul Jetley
This paper presents our effort of using model-driven engineering to establish a safety-assured implementation of Patient-Controlled Analgesic (PCA) infusion pump software based on the generic PCA reference model provided by the U.S. Food and Drug Administration (FDA). The reference model was first translated into a network of timed automata using the UPPAAL tool. Its safety properties were then assured according to the set of generic safety requirements also provided by the FDA. Once the safety of the reference model was established, we applied the TIMES tool to automatically generate platform-independent code as its preliminary implementation. The code was then equipped with auxiliary facilities to interface with pump hardware and deployed onto a real PCA pump. Experiments show that the code worked correctly and effectively with the real pump. To assure that the code does not introduce any violation of the safety requirements, we also developed a testbed to check the consistency between the reference model and the code through conformance testing. Challenges encountered and lessons learned during our work are also discussed in this paper.
[AVS11]
Biomedical Devices and Systems Security
David Arney, Krishna K. Venkatasbramanian, Oleg Sokolsky, and Insup Lee
Medical devices have been changing in revolutionary ways in recent years. One is in their form-factor. Increasing miniaturization of medical devices has made them wearable, light-weight, and ubiquitous; they are available for continuous care and not restricted to clinical settings. Further, devices are increasingly becoming connected to external entities through both wired and wireless channels. These two developments have tremendous potential to make healthcare accessible to everyone and reduce costs. However, they also provide increased opportunity for technology savvy criminals to exploit them for fun and profit. Consequently, it is essential to consider medical device security issues.
In this paper, we focused on the challenges involved in securing networked medical devices. We provide an overview of a generic networked medical device system model, a comprehensive attack and adversary model, and describe some of the challenges present in building security solutions to manage the attacks. Finally, we provide an overview of two areas of research that we believe will be crucial for making medical device system security solutions more viable in the long run: forensic data logging, and building security assurance cases.
[KRA10]
GSA: A Framework for Rapid Prototyping of Smart Alarm Systems
Andrew King, Alex Roederer, David Arney, Sanjian Chen, Margaret Fortino-Mullen, Ana Giannareas, C. William Hanson III, Vanessa Kern, Nicholas Stevens, Jonathan Tannen, Adrian Viesca Trevino, Soojin Park, Oleg Sokolsky, and Insup Lee
We describe the Generic Smart Alarm, an architectural framework for the development of decision support modules for a variety of clinical applications. The need to quickly process patient vital signs and detect patient health events arises in many clinical scenarios, from clinical decision support to tele-health systems to home-care applications. The events detected during monitoring can be used as caregiver alarms, as triggers for further downstream processing or logging, or as discrete inputs to decision support systems or physiological closed-loop applications.
We believe that all of these scenarios are similar, and share a common framework of design. In attempting to solve a particular instance of the problem, that of device alarm fatigue due to numerous false alarms, we devised a modular system based around this framework. This modular design allows us to easily customize the framework to address the specific needs of the various applications, and at the same time enables us to perform checking of consistency of the system.
In the paper we discuss potential specific clinical applications of a generic smart alarm framework, present the proposed architecture of such a framework, and motivate the benefits of a generic framework for the development of new smart alarm or clinical decision support systems.
[MRK11]
On Effective Testing of Health Care Simulation Software
Christian Murphy, M.S. Raunak, Andrew King, Sanjian Chen, Christopher
Imbriano, Gail Kaiser, Insup Lee, Oleg Sokolsky, Lori Clarke, Leon
Osterweil
Health care professionals rely on software to simulate anatomical and physiological elements of the human body for purposes of training, prototyping, and decision making. Software can also be used to simulate medical processes and protocols to measure cost effectiveness and resource utilization. Whereas much of the software engineering research into simulation software focuses on validation (determining that the simulation accurately models real-world activity), to date there has been little investigation into the testing of simulation software itself, that is, the ability to effectively search for errors in the implementation. This is particularly challenging because often there is no test oracle to indicate whether the results of the simulation are correct. In this paper, we present an approach to systematically testing simulation software in the absence of test oracles, and evaluate the effectiveness of the technique.
[CPL11]
Removing Abstraction Overhead in the Composition of Hierarchical
Real-Time Systems
Sanjian Chen, Linh T. X. Phan, Jaewoo Lee, Insup Lee and Oleg Sokolsky
The hierarchical real-time scheduling framework is a widely accepted model to facilitate the design and analysis of the increasingly complex real-time systems. Interface abstraction and composition are the key issues in the hierarchical scheduling framework analysis. Schedulability is essential to guarantee that the timing requirements of all components are satisfied. In order for the design to be resource efficient, the composition must be bandwidth optimal. Associativity is desirable for open systems in which components may be added or deleted at run time. Previous techniques on compositional scheduling are either not resource efficient in some aspects, or cannot achieve optimality and associativity at the same time. In this paper, several important properties regarding the periodic resource model are identified. Based on those properties, we propose a novel interface abstraction and composition framework which achieves schedulability, optimality, and associativity. Our approach eliminates abstraction overhead in the composition.
[SCV11]
Reputation-based Networked Control with Data-Corrupting Channels
Shreyas Sundaram, Jian Chang, Krishna K. Venkatasubramanian, Chinwendu Enyioha, Insup Lee, George Pappas
We examine the problem of reliable networked control when
the communication channel between the controller and the
actuator periodically drops packets and is faulty i.e., corrupts/
alters data. We first examine the use of a standard
triple modular redundancy scheme (where the control input
is sent via three independent channels) with majority voting
to achieve mean square stability. While such a scheme
is able to tolerate a single faulty channel when there are no
packet drops, we show that the presence of lossy channels
prevents a simple majority-voting approach from stabilizing
the system. Moreover, the number of redundant channels
that are required in order to maintain stability under majority
voting increases with the probability of packet drops.
We then propose the use of a reputation management scheme
to overcome this problem, where each channel is assigned a
reputation score that predicts its potential accuracy based
on its past behavior. The reputation system builds on the
majority voting scheme and improves the overall probability
of applying correct (stabilizing) inputs to the system. Finally,
we provide analytical conditions on the probabilities
of packet drops and corrupted control inputs under which
mean square stability can be maintained, generalizing existing
results on stabilization under packet drops.
[PSC10]
Modeling Buffers with Data Refresh Semantics in Automotive Architectures
Linh T.X. Phan, Reinhard Schneider, Samarjit Chakraborty, and Insup Lee
Automotive architectures consist of multiple electronic control units
(ECUs) which run distributed control applications. Such ECUs are
connected to sensors and actuators and communicate via shared
buses. Resource arbitration at the ECUs and also in the communication
medium, coupled with variabilities in execution requirements
of tasks results in jitter in the signal/data streams existing in
the system. As a result, buffers are required at the ECUs and bus
controllers. However, these buffers often implement different semantics
FIFO queuing, which is the most straightforward buffering
scheme, and data refreshing, where stale data is overwritten by
freshly sampled data. Traditional timing and schedulability analysis
that are used to compute, e.g., end-to-end delays, in such automotive
architectures can only model FIFO buffering. As a result,
they return pessimistic delay and resource estimates because in reality
overwritten data items do not get processed by the system.
In this paper we propose an analytical framework for accurately
modeling such data refresh semantics. Our model exploits a novel
feedback control mechanism and is purely functional in nature. As
a result, it is scalable and does not involve any explicit state modeling. Using this model we can estimate various timing and performance
metrics for automotive ECU networks consisting of buffers
implementing different data handling semantics. We illustrate the
utility of this model through three case studies from the automotive
electronics domain.
[ZPT10]
On the Feasibility of Dynamic Rescheduling on the Intel Distributed Computing Platform
Zhuoyao Zhang, Linh T.X. Phan, Godfrey Tan, Saumya Jain, Harrison Duong, Boon Thau Loo, and Insup Lee
This paper examines the feasibility of dynamic rescheduling techniques
for effectively utilizing compute resources within a data center.
Our work is motivated by practical concerns of Intel’s NetBatch
system, an Internet-scale data center based distributed computing
platform developed by Intel Corporation for massively parallel chip
simulations within the company. NetBatch has been operational for
many years, and currently is deployed live on tens of thousands of
machines that are globally distributed at various data centers. We
perform an analysis of job execution traces obtained over a one
year period collected from tens of thousands of NetBatch machines
from 20 different pools. Our analysis show that we observe that
the NetBatch currently does not make full use of all the resources.
Specifically, the job completion time can be severely impacted due
to job suspension when higher priority jobs preempt lower priority
jobs. We then develop dynamic job rescheduling strategies that
adaptively restart jobs to available resources elsewhere, which better
utilize system resources and improve completion times. Our
trace-driven evaluation results show that dynamic rescheduling enables
NetBatch to significantly reduce system waste and completion
time of suspended jobs.
[PLE10]
CARTS: A Tool for Compositional Analysis of Real-Time Systems
Linh T.X. Phan, Jaewoo Lee, Arvind Easwaran, Vinay Ramaswamy, Sanjian Chen, Insup Lee, and Oleg Sokolsky
This paper demonstrates CARTS, a compositional analysis
tool for real-time systems. We presented an overview of the
underlying theoretical foundation and the architecture design
of the tool. CARTS is open source and available for free
download at http://rtg.cis.upenn.edu/carts/.
[PLS11]
A Semantic Framework for Multi-Mode Systems
Linh T.X. Phan, Insup Lee, and Oleg Sokolsky
We present a unified framework for the specification
and analysis of mode-change protocols used in multi-mode realtime
systems. We propose a highly expressive formalism, called
MCP, to model the system behavior during mode transitions,
and show how various existing mode change protocols can be
described as MCPs. The explicit representation of the MCP
model provides a means to analyze the system state during a
mode transition as well as during an intra-mode execution. We
introduce the concept of feasibility with respect to the MCP
model, and give a decidable method for checking the feasibility of
a MCP for a given multi-mode system. The formalization of mode
change behaviors using the MCP model allows a range of mode
change protocols to be modeled, evaluated, and optimized to the
specific operations and performance requirements of the system.
Besides feasibility analysis, it is also possible to analyze other
system behaviors (e.g., delay between modes, buffer backlog)
using automata verification techniques. Our framework can
also be used to describe mode change semantics of multi-mode
systems whose modes/transitions have different criticality levels,
or of systems composed of multiple multi-mode components that
require different mode change protocols.
[DJL11]
Permission to speak: A logic for access control and conformance
Nikhil Dinesh, Aravind Joshi, Insup Lee, and Oleg Sokolsky
Formal languages for policy have been developed for access control and conformance checking. In this paper, we describe a formalism that combines features that have been developed for each application. From access control, we adopt the use of a saying operator. From conformance checking, we adopt the use of operators for obligation and permission. The operators are combined using an axiom that permits a principal to speak on behalf of another. The combination yields benefits to both applications. For access control, we overcome the problematic interaction between hand-off and classical reasoning. For conformance, we obtain a characterization of legal power by nesting saying with obligation and permission.
The axioms result in a decidable logic. We integrate the axioms into a logic programming approach, which lets us use quantification in policies while preserving decidability of access control decisions. Conformance checking, in the presence of nested obligations and permissions, is shown to be decidable. Non-interference is characterized using reachability via permitted statements.
[LES09]
Multiprocessor Real-Time Scheduling Considering Concurrency
and Urgency
Jinkyu Lee, Arvind Easwaran, Insik Shin, and Insup Lee
It has been widely studied how to schedule real-time tasks on multiprocessor platforms. Several studies find optimal scheduling policies for implicit deadline task systems, but it is hard to understand how each policy utilizes the two important aspects of scheduling real-time tasks on multiprocessors: inter-job concurrency and job urgency. In this paper, we introduce a new scheduling policy that considers these two properties. We prove that the policy is optimal for the special case when the execution time of all tasks are equally one and deadlines are implicit, and observe that the policy is a new concept in that it is not an instance of Pfair or ERfair. It remains open to find a scheduliability condition for general task systems under our scheduling policy.
[WAC10]
Spam Mitigation using Spatio-Temporal Reputations from Blacklist History
Andrew G. West, Adam J. Aviv, Jian Chang, and Insup Lee
IP blacklists are a spam filtering tool employed by a large number of email providers. Centrally maintained and well regarded, blacklists can filter 80+% of spam without having to perform computationally expensive content-based filtering. However, spammers can vary which hosts send spam (often in intelligent ways), and as a result, some percentage of spamming IPs are not actively listed on any blacklist. Blacklists also provide a previously untapped resource of rich historical information. Leveraging this history in combination with spatial reasoning, this paper presents a novel reputation model (PreSTA), designed to aid in spam classification. In simulation on arriving email at a large university mail system, PreSTA is capable of classifying up to 50% of spam not identified by blacklists alone, and 93% of spam on average (when used in combination with blacklists). Further, the system is consistent in maintaining this blockage-rate even during periods of decreased blacklist performance. PreSTA is scalable and can classify over 500,000 emails an hour. Such a system can be implemented as a complementary blacklist service and used as a first-level filter or prioritization mechanism on an email server.
[WKL10c]
STiki: An Anti-Vandalism Tool for Wikipedia using Spatio-Temporal
Analysis of Revision Metadata
Andrew G. West, Sampath Kannan, and Insup Lee
STiki is an anti-vandalism tool for Wikipedia. Unlike similar tools, STiki does not rely on natural language processing (NLP) over the article or diff text to locate vandalism. Instead, STiki leverages spatio-temporal properties of revision metadata. The feasibility of utilizing such properties was demonstrated in our prior work, which found they perform comparably to NLP-efforts while being more efficient, robust to evasion, and language independent.
STiki is a real-time, on-Wikipedia implementation based on these properties. It consists of, (1) a server-side processing engine that examines revisions, scoring the likelihood each is vandalism, and, (2) a client-side GUI that presents likely vandalism to end-users for definitive classiffcation (and if necessary, reversion on Wikipedia). Our demonstration will provide an introduction to spatio-temporal properties, demonstrate the STiki software, and discuss alternative research uses for the open-source code.
[WKL10b]
Spatio-Temporal Analysis of Wikipedia Metadata and the STiki Anti-Vandalism Tool
Andrew G. West, Sampath Kannan, and Insup Lee
The bulk of Wikipedia anti-vandalism tools require natural language processing over the article or diff text. However, our prior work demonstrated the feasibility of using spatio-temporal properties to locate malicious edits. STiki is a real-time, on-Wikipedia tool leveraging this technique.
The associated poster reviews STiki's methodology and performance. We find competing anti-vandalism tools inhibit maximal performance. However, the tool proves particularly adept at mitigating long-term embedded vandalism. Further, its robust and language-independent nature make it well-suited for use in less-patrolled Wiki installations.
[PLS10]
A Process Algebraic Framework for Modeling Resource Demand and Supply
Anna Philippou, Insup Lee, Oleg Sokolsky, and Jin-Young Choi
As real-time embedded systems become more complex, resource partitioning is increasingly used to guarantee real-time performance. Recently, several compositional frameworks of resource partitioning have been proposed using real-time scheduling theory with various notions of real-time tasks running under restricted resource supply environments. However, these approaches are limited in their expressiveness in that they are capable of describing resource-demand tasks, but not resource supplies.
This paper describes a process algebraic framework for reasoning about resource demand and supply inspired by the timed process algebra ACSR. In ACSR, realtime tasks are specified by enunciating their consumption needs for resources.
To also accommodate resource-supply processes we define PADS where, in addition to ACSR-like resource requests, we can specify availability of a resource in a given time step. Using PADS, we define a supply-demand relation where a pair (S; T) belongs to the relation if the demand process T can be scheduled under supply S. We develop a theory of compositional schedulability analysis as well as a technique for synthesizing an optimal supply process for a set of tasks. We illustrate our technique via a number of examples.
[LPC10]
Improving Resource Utilization for Compositional Scheduling using
DPRM Interfaces
Jaewoo Lee, Linh T.X. Phan, Sanjian Chen, Oleg Sokolsky, and Insup Lee
The paper revisits the generation of interfaces for compositional real-time scheduling. Following an established line of research, we use periodic resource models in component interfaces to describe resource demand of the component. We identify a deficiency of existing interface generation algorithms that may require parameters of the resource model to be infeasibly small. We propose a new algorithm for interface generation that avoids this deficiency. We further demonstrate that resource utilization can be improved by using dual-periodic resource model (DPRM) interfaces that employ two periodic resource models to characterize the resource demand more precisely.
[AFH10]
Generating Reliable Code from Hybrid-Systems Models
Madhukar Anand, Sebastian Fischmeister, Yerang Hur, Jesung Kim,
and Insup Lee
Hybrid systems have emerged as an appropriate formalism to model embedded systems as they capture the theme of continuous dynamics with discrete control. Under this paradigm, distributed embedded systems can be modeled as a network of communicating hybrid automata. Several techniques for code generation from these models have also been proposed and commercially implemented. Providing formal guarantees of the generated code with respect to the model, however, has turned out to be a hard problem. While the model is set in continuous time with concurrent execution and instantaneous switching, the code running on an inherently discrete platform, can be affected by the sampling interval, round-off errors, and communication delays between the sensor, controller, and actuators. Consequently, semantic differences between the model and its code can arise with potentially different system behavior. This paper proposes a criterion for faithful implementation of the hybrid-systems model with a focus on its switching semantics. We discuss different techniques to ensure a faithful implementation of the model, and test the feasibility of our concepts by implementing a model heater system. In this heater case study, we successfully eliminate all fault transitions and, thereby, generate code with correct behavior complying with the specification.
[AFL10]
Model-based Programming of Modular Robots
David Arney, Sebastian Fischmeister, Insup Lee, Yoshihito Takashima,
Mark Yim
Modular robots are a powerful concept for robotics. A modular robot consists of many individual modules so it can adjust its configuration to the problem. However, the fact that a modular robot consists of many individual modules makes it a highly distributed, highly concurrent real-time system, which are notoriously hard to program. In this work, we present our programming framework for writing control applications for modular robots. The framework includes a toolset that allows a model-based programing approach for control application of modular robots with code generation and verification. The framework is characterized by the following three features. First, it provides a complex programming model that is based on standard finite state machines extended in syntax and semantics to support communication, variables, and actions. Second, the framework provides compositionality at the hardware and at the software level and allows building the modular robot and its control application from small building blocks. And third, the framework supports formal verification of the control application to aid the gait and task developer in identifying problems and bugs before the deployment and testing on the physical robot.
[RLS10]
Cyber-physical systems: the next computing revolution
Ragunathan (Raj) Rajkumar, Insup Lee, Lui Sha, and John Stankovic
Cyber-physical systems (CPS) are physical and engineered systems whose
operations are monitored, coordinated, controlled and integrated by a
computing and communication core. Just as the internet transformed how
humans interact with one another, cyber-physical systems will transform how
we interact with the physical world around us. Many grand challenges await
in the economically vital domains of transportation, health-care,
manufacturing, agriculture, energy, defense, aerospace and buildings. The
design, construction and verification of cyber-physical systems pose a
multitude of technical challenges that must be addressed by a
cross-disciplinary community of researchers and educators.
[LeSo10]
Medical Cyber Physical Systems
Insup Lee and Oleg Sokolsky
We discuss current trends in the development and use of high-confidence
medical cyber physical systems (MCPS). These trends, including increased
reliance on software to deliver new functionality, wider use of network
connectivity in MCPS, and demand for continuous patient monitoring, bring
new challenges into the process of MCPS development and at the same time
create new opportunities for research and development.
[JKC10]
Automated Test Coverage Measurement for Reactor Protection System
Software implemented in Function Block Diagram
Eunkyoung Jee, Suin Kim, Sungdeok Cha, and Insup Lee
We present FBDTestMeasurer, an automated test coverage measurement
tool for function block diagram (FBD) programs which are increasingly used
in implementing safety critical systems such as nuclear reactor protection
systems. We have defined new structural test coverage criteria for FBD
programs in which dataflow-centric characteristics of FBD programs were well
reflected. Given an FBD program and a set of test cases,
FBDTestMeasurer produces test coverage score and uncovered test
requirements with respect to the selected coverage criteria. Visual
representation of uncovered data paths enables testers to easily identify
which parts of the program need to be tested further. We found many aspects
of the FBD logic that were not tested sufficiently when conducting a case
study using test cases prepared by domain experts for reactor protection
system software. Domain experts found this technique and tool highly
intuitive and useful to measure the adequacy of FBD testing and generate
additional test cases.
[JWK10]
A Safety-Assured Development Approach for Real-Time Software
Eunkyoung Jee, Shaohui Wang, Jeong Ki Kim, Jaewoo Lee, Oleg Sokolsky,
and Insup Lee
Guaranteeing timing properties is an important issue as we develop
safety-critical real-time systems such as cardiac pacemakers. We present a
safety assured development approach of real-time software using a pacemaker
as our case study. Following the model-driven development techniques,
measurement-based timing analysis is used to guarantee timing properties in
implementation as well as in the formal model. Formal specification with
timed automata is checked with respect to timing properties by model checking
technique and is transformed into implementation systematically. When timing
properties may be violated in the implementation due to timing delay, it is
suggested to measure the time deviation and reflect it to the code explicitly
by modifying guards. The model is altered according to the modifications in
the code. These changes of the code and the model are considered safe if
all the properties are still satisfied by the modified model in re-performed
model hecking. We demonstrate how the suggested approach can be applied to
single-threaded and multi-threaded versions of implementation. This approach
can provide developers with a useful time-guaranteeing technique applicable
to several code generation schemes without imposing many restrictions.
[PLS10]
Compositional Analysis of Multi-Mode Systems
Linh T.X. Phan, Insup Lee, and Oleg Sokolsky
The paper presents a model for multi-mode realtime
applications and develops new techniques for the compositional
analysis of systems that contain multiple such applications.
An algorithm for constructing an interface for a single multimode
application is presented. Then, a method for computing
an interface of a composite application is presented, which uses
only the interfaces of constituent applications. A case study of an
adaptive streaming system demonstrates that multi-mode analysis
offers more precise results compared to a unimodal worst-case
analysis.
[KAL10]
Prototyping Closed Loop Physiologic Control with the Medical Device Coordination Framework
Andrew King, Dave Arney, Insup Lee, Oleg Sokolsky, John Hatcliff, and Sam Proctor
Medical devices historically have been monolithic units – developed,
validated, and approved by regulatory authorities as standalone
entities. Despite the fact that modern medical devices increasingly
incorporate connectivity mechanisms that enable device
data to be streamed to electronic health records and displays that
aggregate data from multiple devices, connectivity is not being
leveraged to allow an integrated collection of devices to work together
as a single system to automate clinical work flows. This
is due, in part, to current regulatory policies which prohibit such
interactions due to safety concerns.
In previous work, we proposed an open source middleware framework
and an accompanying model-based development environment
that could be used to quickly implement medical device coordination
applications – enabling a “systems of systems” paradigm for
medical devices. Such a paradigm shows great promise for supporting
many applications that increase both the safety and effectiveness
of medical care as well as the efficiency of clinical workflows.
In this paper, we report on our experience using our Medical
Device Coordination Framework (MDCF) to carry out a rapid prototyping
of one such application – a multi-device medical system
that uses closed loop physiologic control to a affect better patient
outcomes for Patient Controlled Anelgesic (PCA) pumps.
[WKL10a]
Detecting Wikipedia Vandalism via Spatio-Temporal Analysis
of Revision Metadata
Andrew G. West, Sampath Kannan, and Insup Lee
Blatantly unproductive edits undermine the quality of the
collaboratively-edited encyclopedia, Wikipedia. They not
only disseminate dishonest and offensive content, but force
editors to waste time undoing such acts of vandalism. Language-
processing has been applied to combat these malicious
edits, but as with email spam, these filters are evadable and
computationally complex. Meanwhile, recent research has
shown spatial and temporal features effective in mitigating
email spam, while being lightweight and robust.
In this paper, we leverage the spatio-temporal properties
of revision metadata to detect vandalism on Wikipedia. An
administrative form of reversion called rollback enables the
tagging of malicious edits, which are contrasted with nonoffending
edits in numerous dimensions. Crucially, none of
these features require inspection of the article or revision
text. Ultimately, a classifier is produced which flags vandalism
at performance comparable to the natural-language efforts
we intend to complement (85% accuracy at 50% recall).
The classifier is scalable (processing 100+ edits a second)
and has been used to locate over 5,000 manually-confirmed
incidents of vandalism outside our labeled set.
[APG10]
Toward Patient Safety in Closed-Loop Medical Device Systems
David Arney, Miroslav Pajic, Julian M. Goldman, Insup Lee,
Rahul Mangharam, and Oleg Sokolsky
A model-driven design and validation of closed-loop medi-
cal device systems is presented. Currently, few if any med-
ical systems on the market support closed-loop control of
interconnected medical devices, and mechanisms for regu-
latory approval of such systems are lacking. We present a
system implementing a clinical scenario where closed-loop
control may reduce the possibility of human error and im-
prove safety of the patient. The safety of the system is stud-
ied with a simple controller proposed in the literature. We
demonstrate that, under certain failure conditions, safety
of the patient is not guaranteed. Finally, a more complex
controller is described and ensures safety even when failures
are possible. This investigation is an early attempt to intro-
duce automatic control in clinical scenarios and to delineate
a methodology to validate such patient-in-the-loop systems
for safe and correct operation.
[ESS07]
Schedulability Analysis of Hierarchical Real-Time Systems
Arvind Easwaran, Insik Shin, Oleg Sokolsky, and Insup Lee
Embedded systems are complex as a whole but consist of smaller independent modules interacting with each other. This structure makes embedded systems amenable to compositional design. Real-time embedded systems consist of real-time workloads having temporal deadlines. Compositional design of real-time embedded systems can be done using systems consisting of real-time components arranged in a scheduling hierarchy. Each component consists of some real-time workload and a scheduling policy for the workload. To simplify schedulability analysis for such systems, analysis can be done compositionally using interfaces that abstract the timing requirements of components. To facilitate analysis of dynam- ically changing real-time systems, the framework must support incremental analysis. In this paper, we summarize our work [19, 6] on schedulability analysis for hierarchical real-time systems. We describe a compositional analysis technique that abstracts resource requirements of components using periodic resource models. To support incremental analysis and resource bandwidth minimization, we describe an extension to this interface model. Each extended interface consists of multiple periodic resource models for different periods. This allows the selection of a periodic model that can schedule the system using minimum bandwidth. We also account for context switch overheads in these interfaces. We then describe an associative composition technique for such interfaces that supports incremental analysis.
[PCL09]
Timing Analysis of Mixed Time/Event-Triggered Multi-Mode Systems
Linh T.X. Phan, Samarjit Chakraborty, and Insup Lee
Many embedded systems operate in multiple modes,
where mode switches can be both time- as well as event-triggered.
While timing and schedulability analysis of the system when it
is operating in a single mode has been well studied, it is always
difficult to piece together the results from different modes in
order to deduce the timing properties of a multi-mode system.
As a result, often certain restrictive assumptions are made,
e.g., restricting the time instants at which mode changes might
occur. The problem becomes more complex when both time- and
event-triggered mode changes are allowed. Further, for complex
systems that cannot be described by traditional periodic/sporadic
event models (i.e., where event streams are more complex/bursty)
modeling multiple modes is largely an open problem. In this
paper we propose a model and associated analysis techniques to
describe embedded systems that process multiple bursty/complex
event/data streams and in which mode changes are both timeand
event-triggered. Compared to previous studies, our model is
very general and can capture a wide variety of real-life systems.
Our analysis techniques can be used to determine different
performance metrics, such as the maximum fill-levels of different
buffers and the delays suffered by the streams being processed
by the system. The main novelty in our analysis lies in how
we piece together results from the different modes in order to
obtain performance metrics for the full system. Towards this,
we propose both exact, but computationally expensive, as well
as safe approximation techniques. The utility of our model and
analysis has been illustrated using a detailed smart-phone case
study.
[CLS09]
Model-Based Testing of GUI-Driven Applications
Vivien Chinnapongse, Insup Lee, Oleg Sokolsky, Shaohui Wang, and
Paul L. Jones
While thorough testing of reactive systems is essential to
ensure device safety, few testing methods center on GUI-driven applications.
In this paper we present one approach for the model-based testing
of such systems. Using the AHLTA-Mobile case study to demonstrate
our approach, we first introduce a high-level method of modeling the
expected behavior of GUI-driven applications. We show how to use the
NModel tool to generate test cases from this model and present a way
to execute these tests within the application, highlighting the challenges
of using an API-geared tool in a GUI-based setting. Finally we present
the results of our case study.
[AFG09]
Plug-and-Play for Medical Devices: Experiences from a Case Study
David Arney, Sebastian Fischmeister, Julian M. Goldman, Insup Lee, and Robert Trausmuth
Medical devices are pervasive throughout modern healthcare, but each device works on its own and in isolation. Interoperable medical devices would lead to clear benefits for the care provider and the patient, such as more accurate assessment of the patientœôòùs health and safety interlocks that would enable error-resilient systems. The Center for Integration of Medicine & Innovative Technology (www.CIMIT.org) sponsors the Medical Device Plug-and-Play Interoperability program (www.MDPnP.org), which is leading the development and adoption of standards for medical device interoperability. Such interoperable medical devices will lead to increased patient safety and enable new treatment options, and the aim of this project is to show the benefits of interoperable and interconnected medical devices.
[ELS09]
A Compositional Scheduling Framework for Digital Avionics Systems
Arvind Easwaran, Insup Lee, Oleg Sokolsky and Steve Vestal
ARINC specification 653-2 describes the interface
between application software and underlying middleware in a
distributed real-time avionics system. The real-time workload in
this system comprises of partitions, where each partition consists
of one or more processes. Processes incur blocking and preemption
overheads, and can communicate with other processes in
the system. In this work, we develop compositional techniques
for automated scheduling of such partitions and processes. At
present, system designers manually schedule partitions based on
interactions they have with the partition vendors. This approach
is not only time consuming, but can also result in under utilization
of resources.
[MGL09]
Strong and Weak Policy Relations
Michael J. May, Carl A. Gunter, Insup Lee, and Steve Zdancewic
Access control and privacy policy relations tend to focus on decision outcomes and are very sensitive to defined terms and state. Small changes or updates to a policy language or vocabulary may make two similar policies incomparable. To address this we develop two flexible policy relations derived from bisimulation in process calculi. Strong licensing compares the outcome of two policies strictly, similar to strong bisimulation. Weak licensing compares the outcome of policies more flexibly by ignoring irrelevant (non-conflicting) differences between outcomes, similar to weak bisimulation. We illustrate the relations using examples from P3P.
[SLC09]
Process-Algebraic Interpretation of AADL Models
Oleg Sokolsky, Insup Lee, and Duncan Clarke
We present a toolset for the behavioral verification and validation of architectural models of embedded systems expressed in the language AADL. The toolset provides simulation and timing analysis of AADL models. Underlying both tools is a process-algebraic implementation of AADL semantics. The common implementation of the semantics ensures consistency in the analysis results between the tools.
[WLL09]
Verifiable Policy-based Routing with DRIVER
Anduo Wang, Changbin Liu, Boon Thau Loo, Oleg Sokolsky, and Prithwash Basu
The Internet today runs on a complex routing protocol called the Border Gateway Protocol (BGP). BGP is a policy-based protocol, in which autonomous Internet Service Providers (ISPs) impose their local policies on the propagation of routing information. Over the past few years, there has been a growing consensus on the complexity and fragility of BGP routing. To address these challenges, we present the DRIVER system for designing, analyzing and implementing policy-based routing protocols. Our system utilizes a declarative network verifier (DNV) which leverages declarative networking's connection to logic programming by automatically compiling high-level declarativen networking program into formal specifications, which can be directly used in a theorem prover for verification. In addition to verifying declarative networking programs using a theorem prover, the DRIVER system enables a similar transformation of verified formal specifications limited to fragment of second order logic to declarative networking programs for execution. As our main use case, we demonstrate the verification of a component-based specification of BGP protocol where DRIVER enables the analysis of convergence properties of Internet routing protocols with customizable policy configuration components. We show that the properties verified with DRIVER are indeed preserved in the synthesized implementation by performing experimental evaluation in a local cluster, where the equivalent declarative networking programs derived from the verified specifications displayed consistent behavior with regard to DRIVER verification.
[WKL09]
An Evaluation Framework for Reputation Management Systems
Andrew G. West, Sampath Kannan, Insup Lee, and Oleg Sokolsky
Reputation management (RM) is employed in distributed and peer-to-peer networks to help users compute a measure of trust in other users based on initial belief, observed behavior, and run-time feedback. These trust values influence how, or with whom, a user will interact. Existing literature on RM focuses primarily on algorithm development, not comparative analysis. To remedy this, we propose an evaluation framework based on the trace-simulator paradigm. Trace file generation emulates a variety of network configurations, and particular attention is given to modeling malicious user behavior. Simulation is trace-based and incremental trust calculation techniques are developed to allow experimentation with networks of substantial size. The described framework is available as open source so that researchers can evaluate the effectiveness of other reputation management techniques and/or extend functionality.
This chapter reports on our framework's design decisions. Our goal being to build a general-purpose simulator, we have the opportunity to characterize the breadth of existing RM systems. Further, we demonstrate our tool using two reputation algorithms (EigenTrust and a modified TNA-SL) under varied network conditions. Our analysis permits us to make claims about the algorithms' comparative merits. We conclude that such systems, assuming their distribution is secure, are highly effective at managing trust, even against adversarial collectives.
[WAC09]
QuanTM: A Quantitative Trust Management System
Andrew G. West, Adam J. Aviv, Jian Chang, Vinayak S. Prabhu,
Matt Blaze, Sampath Kannan, Insup Lee, Jonathan M. Smith, and Oleg Sokolsky
Quantitative Trust Management (QTM) provides a dynamic interpretation of
authorization policies for access control decisions based on upon evolving
reputations of the entities involved. QuanTM, a QTM system, selectively
combines elements from trust management and reputation management to create
a novel method for policy evaluation. Trust management, while effective in
managing access with delegated credentials (as in PolicyMaker and KeyNote),
needs greater flexibility in handling situations of partial trust. Reputation
management provides a means to quantify trust, but lacks delegation and policy
enforcement.
This paper reports on QuanTM's design decisions and novel policy evaluation
procedure. A representation of quantified trust relationships, the trust
dependency graph, and a sample QuanTM application specific to the KeyNote
trust management language, are also proposed.
[BKL09]
Dynamic Trust Management
Matt Blaze, Sampath Kannan, Insup Lee, Oleg Sokolsky,
Jonathan M. Smith, Angelos D. Keromytis, Wenke Lee
Trust management forms the basis for communicating policy among system
elements and demands credential checking for access to all virtual private
service resourcesalong with careful evaluation of credentials against specified
policiesbefore a party can be trusted.
[AFL09]
Resource Scopes: Toward Language Support for Compositional Determinism
Madhukar Anand, Sebastian Fischmeister, and Insup Lee
Complex real-time embedded systems should be compositional
and deterministic in the resource, time, and value
domains. Determinism eases the engineering of correct systems
and compositionality simplifies the assembly of complex
systems out of smaller modules. This paper describes the
PEACOD framework that is developed to support deterministic
behavior for resource consumption, value passing, and
timing. The paper introduces the notions of determinism
in the context of the resource, value, and temporal domains,
and present the resource-scope language construct
that can be used to program such deterministic behaviors.
Furthermore, the paper also provides semantics for the
resource scope construct and uses these semantics to show
that the program behavior is preserved under composition.
The paper briefly describes the current implementation of
PEACOD.
[AGW09]
Synchronizing an X-ray and Anesthesia Machine Ventilator: A Medical Device Interoperability Case Study
David Arney, Julian M. Goldman, Susan F. Whitehead and Insup Lee
When a x-ray image is needed during surgery, clinicians may stop the
anesthesia machine ventilator while the exposure is made. If the ventilator is
not restarted promptly, the patient may experience severe complications.
This paper explores the interconnection of a ventilator and simulated x-ray
into a prototype plug-and-play medical device system. This work assists
ongoing interoperability framework development standards efforts
to develop functional and non-functional requirements and illustrates the
potential patient safety benefits of interoperable medical device systems by
implementing a solution to a clinical use case requiring interoperability.
[WBL09]
Declarative Network Verification
Anduo Wang, Prithwish Basu, Boon Thau Loo, Oleg Sokolsky
In this paper, we present our initial design and implementation of a declarative network verifier (DNV). DNV utilizes theorem proving, a well established verification technique where logic-based axioms that automatically capture network semantics are generated, and a user-driven proof process is used to establish network correctness properties. DNV takes as input declarative networking specifications written in the Network Datalog (NDlog) query language, and maps that automatically into logical axioms that can be directly used in existing theorem provers to validate protocol correctness. DNV is a significant improvement compared to existing use case of theorem proving which typically require several man-months to construct the system specifications. Moreover, NDlog, a high-level specification, whose semantics are precisely compiled into DNV without loss, can be directly executed as implementations, hence bridging specifications, verification, and implementation. To validate the use of DNV, we present case studies using DNV in conjunction with the PVS theorem prover to verify routing protocols, including eventual properties of protocols in dynamic settings.
[DJL07]
Logic-based Regulatory Conformance Checking
Nikhil Dinesh, Aravind Joshi, Insup Lee, and Oleg Sokolsky
In this paper, we describe an approach to formally assess whether an organization conforms to a body of regulation. Conformance is cast as a model checking question where the regulation is represented in a logic that is evaluated against an abstract model representing the operations of an organization. Regulatory bases are large and complex, and the long term goal of our work is to be able to use natural language processing (NLP) to assist in the translation of regulation to logic. We argue that the translation of regulation to logic should proceed one sentence at a time. A challenge in taking this approach arises from the fact that sentences is regulation often refer to others. We motivate the need for a formal representation of regulation to accommodate references between statements. We briefly describe a logic in which statements can refer to and reason about others. We then discuss preliminary work on using NLP to assist in the translation of regulatory sentences into logic.
[SoCh08]
Analysis of AADL Models Using Real-Time Calculus with Applications to
Wireless Architectures
Oleg Sokolsky and Alexander Chernoguzov
Architecture Analysis and Design Language (AADL) captures both platform and software architectures of embedded systems in a component oriented fashion. Properties embedded in an AADL model enable several high-level analysis techniques. In this work, we explore how to perform analysis of end-to-end timing characteristics of an AADL model using Real-Time Calculus (RTC). We identify properties of AADL models that are necessary to enable such analysis and develop an algorithm to transform an AADL model into an RTC model.
[FLT08]
Hardware Acceleration for Verifiable, Adaptive Real-Time Communication
Sebastian Fischmeister, Insup Lee, and Robert Trausmuth
Distributed real-time applications implement distributed applications with timeliness requirements. Such systems require a deterministic communication medium with bounded communication delays. Ethernet is a widely used commodity network with a large number of appliances and network components and represents a natural fit for real-time application; unfortunately, standard Ethernet provides no bounded communication delays.
Network Code Processor is a soft processor implementation for real-time communication on Ethernet. The system provides a smart network-card functionality and can be seen as a co-processor for time-triggered communication. Its most distinguishing feature, the programmability of the processor via the Network Code language, allows developers to write adaptive but verifiable communication schedules tailored to the application needs. In this work we present results around the development of the soft processor, discuss the specific challenges of how to build a reliable and fast communication system, the tradeoffs involved when moving from a generic software prototype to a programmable hardware implementation.
[SEL08]
Hierarchical Scheduling Framework for Virtual Clustering of Multiprocessors
Insik Shin, Arvind Easwaran, Insup Lee
Scheduling of sporadic task systems on multiprocessor platforms is an area which has received much attention in the recent past. It is widely believed that finding an optimal scheduler is hard, and therefore most studies have focused on developing algorithms with good utilization bounds. These algorithms can be broadly classified into two categories: partitioned scheduling in which tasks are statically assigned to individual processors, and global scheduling in which each task is allowed to execute on any processor in the platform. In this paper we consider a third, more general, approach called cluster-based scheduling. In this approach each task is statically assigned to a processor cluster, tasks in each cluster are globally scheduled among themselves, and clusters in turn are scheduled on the multiprocessor platform. We develop techniques to support such cluster-based scheduling algorithms, and also consider properties that minimize processor utilization of individual clusters. Since neither partitioned nor global strategies dominate over the other, cluster-based scheduling is a natural direction for research towards achieving improved utilization bounds.
[ShLe08]
Compositional Real-Time Scheduling Framework with Periodic Model
Insik Shin and Insup Lee
It is desirable to develop large complex systems using components based on systematic abstraction and composition. Our goal is to develop a compositional real-time scheduling framework to support abstraction and composition techniques for real-time aspects of components. In this paper, we present a formal description of compositional real-time scheduling problems, which are the component abstraction and composition problems. We identify issues that need be addressed by solutions and provide our framework for the solutions, which is based on the periodic interface. Specifically, we introduce the periodic resource model to characterize resource allocations provided to a single component. We present exact schedulability conditions for the standard Liu and Layland periodic task model and the proposed periodic resource model under EDF and RM scheduling, and we show that the component abstraction and composition problems can be addressed with periodic interfaces through the exact schedulability conditions. We also provide the utilization bounds of a periodic task set over the periodic resource model and the abstraction bounds of periodic interfaces for a periodic task set under EDF and RM scheduling. We finally present the analytical bounds of overheads that our solution incurs in terms of resource utilization increase and evaluate the overheads through simulations.
[LSK08]
A design framework for real-time embedded systems with code size and energy
constraints
Sheayun Lee, Insik Shin, Woonseok Kim, Insup Lee, Sang L. Min
Real-time embedded systems are typically constrained in terms of three system performance criteria: space, time, and energy. The performance requirements are directly translated into constraints imposed on the system's resources, such as code size, execution time, and energy consumption. These resource constraints often interact or even conflict with each other in a complex manner, making it difficult for a system developer to apply a well-defined design methodology in developing a real-time embedded system. Motivated by this observation, we propose a design framework that can flexibly balance the tradeoff involving the system's code size, execution time, and energy consumption. Given a system specification and an optimization criteria, the proposed technique generates a set of design parameters in such a way that a system cost function is minimized while the given resource constraints are satisfied. Specifically, the technique derives code generation decision for each task so that a specific version of code is selected among a number of different ones that have distinct characteristics in terms of code size and execution time. In addition, the design framework determines the voltage/frequency setting for a variable voltage processor whose supply voltage can be adjusted at runtime in order to minimize the energy consumption while execution performance is degraded accordingly. The proposed technique formulates this design process as a constrained optimization problem. We show that this optimization problem is NP-hard and then provide a heuristic solution to it. We show that these seemingly conflicting design goals can be pursued by using a simple optimization algorithm that works with a single optimization criteria. Moreover, the optimization is driven by an abstract system specification given by the system developer, so that the system development process can be automated. The results from our simulation show that the proposed algorithm finds a solution that is close to the optimal one with the average error smaller than 1.0%.
[DJL08]
Reasoning about Conditions and Exceptions to Laws in Regulatory Conformance
Checking
Nikhil Dinesh, Aravind K. Joshi, Insup Lee, and Oleg Sokolsky
This paper considers the problem of checking whether an organization conforms to a body of regulation. Conformance is cast as a trace checking question the regulation is represented in a logic that is evaluated against an abstract trace or run representing the operations of an organization. We focus on a problem in designing a logic to represent regulation.
A common phenomenon in regulatory texts is for sentences to refer to others for conditions or exceptions. We motivate the need for a formal representation of regulation to accommodate such references between statements. We then extend linear temporal logic to allow statements to refer to others. The semantics of the resulting logic is defined via a combination of techniques from Reiter's default logic and Kripke's theory of truth.
[ELS08]
Interface Algebra for Analysis of Hierarchical Real-Time Systems
Arvind Easwaran, Insup Lee, Oleg Sokolsky
Complex real-time embedded systems can be developed using component based design methodologies. Timing requirements of real-time components in the system can be modeled using hierarchical frameworks to capture resource sharing among components under different schedulers. To support component based design for real-time embedded systems, we must then address schedulability analysis of hierarchical scheduling models. In this paper, we propose a generic interface algebra for compositional schedulability analysis of such models. We also define conditions under which this algebra supports incremental analysis, dynamic adaptability, and independent implementability. Furthermore, we also propose a novel periodic resource model based framework for compositional and incremental schedulability analysis of hierarchical scheduling models. This extends our earlier proposed framework with a technique that allows periodic resource models with different periods to be composed together. We formulate this framework in our proposed algebra to demonstrate ease of use of the algebra and to identify framework properties.
[AnLe08]
Robust and Sustainable Schedulability Analysis of Embedded Software
Madhukar Anand and Insup Lee
For real-time systems, most of the analysis involves efficient or exact schedulability checking. While this is important, analysis is often based on the assumption that the task parameters such as execution requirements and inter-arrival times between jobs are known exactly. In most cases, however, only a worst-case estimate of these quantities is available at the time of analysis. It is therefore imperative that schedulability analysis hold for better parameter values (Sustainable Analysis). On the other hand, if the task or system parameters turn out to be worse off, then the analysis should tolerate some deterioration (Robust Analysis). Robust analysis is especially important, because the implication of task schedulability is often weakened in the presence of optimizations that are performed on its code, or dynamic system parameters.
In this work, we define and address sustainability and robustness questions for analysis of embedded real-time software that is modeled by conditional real-time tasks. Specifically, we show that, while the analysis is sustainable for changes in the task such as lower job execution times and increased relative deadlines, it is not the case for code changes such as job splitting and reordering. We discuss the impact of these results in the context of common compiler optimizations, and then develop robust schedulability techniques for operations where the original analysis is not sustainable.
[AEF08]
Compositional Feasibility Analysis for Conditional Task Models
Madhukar Anand, Arvind Easwaran, Sebastian Fischmeister and Insup Lee
Conditional real-time task models, which are generalizations
of periodic, sporadic, and multi-frame tasks, represent
real world applications more accurately. These models
can be classified based on a tradeoff in two dimensions
expressivity and hardness of schedulability analysis. In
this work, we introduce a class of conditional task models
and derive efficient schedulability analysis techniques for
them. These models are more expressive than existing models
for which efficient analysis techniques are known. In this
work, we also lay the groundwork for schedulability analysis
of hierarchical scheduling frameworks with conditional
task models. We propose techniques that abstract timing
requirements of conditional task models, and support compositional
analysis using these abstractions.
[DJL08]
Checking Traces for Regulatory Conformance
Nikhil Dinesh, Aravind K. Joshi, Insup Lee, and Oleg Sokolsky
We consider the problem of checking whether the operations of an organization conform to a body of regulation. The immediate motivation comes from the analysis of the U.S. Food and Drug Administration regulations that apply to bloodbanks - organizations that collect, process, store, and use donations of blood and blood components. Statements in such regulations convey constraints on operations or sequences of operations that are performed by an organization. It is natural to express these constraints in a temporal logic.
There are two important features of regulatory texts that need to be accommodated by a representation in logic. First, the constraints conveyed by regulation can be obligatory (required) or permitted (optional). Second, statements in regulation refer to others for conditions or exceptions. An organization conforms to a body of regulation if and only if it satisfies all the obligations. However, permissions provide exceptions to obligations, indirectly affecting conformance.
In this paper, we extend linear temporal logic to distinguish between obligations and permissions, and to allow statements to refer to others. While the resulting logic allows for a direct representation of regulation, evaluating references between statements has high complexity. We discuss an empirically motivated assumption that lets us replace references with tests of lower complexity, leading to efficient trace-checking algorithms in practice.
[AJJ07]
Formal Methods Based Development of a PCA Infusion Pump Reference Model:
Generic Infusion Pump (GIP) Project
David Arney, Raoul Jetley, Paul Jones, Insup Lee, Oleg Sokolsky
As software becomes ever more ubiquitous and complex in medical devices, it
becomes increasingly important to assure that it performs safely and
effectively. The critical nature of medical devices necessitates that the
software used therein be reliable and free of errors. It becomes imperative,
therefore, to have a conformance review process in place to ascertain the
correctness of the software and to ensure that it meets all requirements and
standards.
Formal methods have long been suggested as a means to design and develop
medical device software. However, most manufacturers shy from using these
techniques, citing them as too complex and time consuming. As a result,
(potentially life-threatening) errors are often not discovered until a
device is already on the market.
In this paper we present a safety model based approach to software conformance
checking. Safety models enable the application of formal methods to software
conformance checking, and provide a framework for rigorous testing. To
illustrate the approach, we develop the safety model for a Generic Infusion
Pump (GIP), and explain how it can be used to aid software conformance
checking in a regulatory environment.
[PS07]
Process-Algebraic Analysis of Timing and Schedulability Properties
Anna Philippou and Oleg Sokolsky
In this chapter, we present an overview of how timing information
can be embedded in process-algebraic frameworks. We concentrate on
the case of discrete-time modeling. We begin by discussing design
approaches that have been adopted in different formalisms to model
time and time passage, and how the resulting mechanisms interact
with one another and with standard untimed process-algebraic
operators. We proceed to give an overview of ACSR, a timed process
algebra developed for modeling and reasoning about timed,
resource-constrained systems. In doing this, ACSR adopts the
notion of a resource as a first-class entity, and it
replaces maximal progress, employed by other timed process
algebras, by the notion of resource-constrained progress.
ACSR associates resource-usage with time passage, and implements
appropriate semantic rules to ensure that progress in the system
is enforced as far as possible while simultaneous usage of a
resource by distinct processes is excluded. In addition, ACSR
employs the notion of priorities to arbitrate access to resources
by competing processes. Finally, we illustrate the use of ACSR for
the schedulability analysis of a realistic real-time system
problem.
[SLS07]
Statistical Runtime Checking of Probabilistic Properties
Usa Sammapun, Insup Lee, Oleg Sokolsky, and John Regehr
Probabilistic correctness is an important aspect of
reliable systems. A soft real-time system, for instance,
may be designed to tolerate some degree of deadline misses under a
threshold.
Since probabilistic systems may behave differently from their
probabilistic models depending on their current environments, checking
the systems at runtime can provide another level of assurance for
their probabilistic correctness. This paper presents a statistical
runtime verification for probabilistic properties using statistical
analysis. However, while this statistical analysis collects a number
of execution paths as samples to check probabilistic properties within
some certain error bounds, runtime verification can only produce one
single sample. This paper provides a technique to produce such a
number of samples and applies this methodology to check probabilistic
properties in wireless sensor network applications.
[EAL07]
Compositional Analysis Framework using EDP Resource Models
Arvind Easwaran, Madhukar Anand, and Insup Lee
Compositional schedulability analysis of hierarchical
scheduling frameworks is a well studied problem, as it
has wide-ranging applications in the embedded systems domain.
Several techniques, such as periodic resource model
based abstraction and composition, have been proposed for
this problem. However these frameworks are sub-optimal
because they incur bandwidth overhead. In this work, we
introduce the Explicit Deadline Periodic (EDP) resource
model, and present compositional analysis techniques under
EDF and DM. We show that these techniques are bandwidth
optimal, in that they do not incur any bandwidth overhead
in abstraction or composition. Hence, this framework
is more efficient when compared to existing approaches.
[FSL07]
A Verifiable Language for Programming Communication Schedules
S. Fischmeister, O. Sokolsky, and I. Lee
Distributed hard real-time systems require predictable communication at the
network level and verifiable communication behavior at the application level.
At the network level, communication between nodes must be guaranteed to happen
within bounded time and one common approach is to restrict the network access
by enforcing a time-division multiple access (TDMA) schedule. At the
application level, the application's communication behavior should be
verified to ensure that the application uses the predictable communication in
the intended way. Network Code is a domain-specific programming language to
write a predictable verifiable distributed communication for distributed
real-time applications. In this paper, we present the syntax and semantics of
Network Code, how we can implement different scheduling policies, and how we
can use tools such as model checking to formally verify the properties of
Network Code programs. We also present an implementation of a runtime system
for executing Network Code on top of RTLinux and measure the overhead incurred
from the runtime system.
[AAF07]
A Dynamic Scheduling Approach to Designing Flexible Safety-Critical
Systems
L. Almeida, M. Anand, S. Fischmeister, and I. Lee
The design of safety-critical systems has typically adopted static techniques
to simplify error detection and fault tolerance. However, economic pressure
to reduce costs is exposing the limitations of those techniques in terms of
efficiency in the use of system resources. In some industrial domains, such
as the automotive, this pressure is too high, and other approaches to safety
must be found, e.g., capable of providing some kind of fault tolerance but
with graceful degradation to lower costs, or also capable of adapting to
instantaneous requirements to better use the computational/communication
resources.
This paper analyzes the development of systems that exhibit such level of
flexibility, allowing the system configuration to evolve within a well-defined
space. Two options are possible, one starting from the typical static
approach but introducing choice points that are evaluated only at runtime,
and another one starting from an open systems approach but delimiting the
space of possible adaptations. The paper follows the latter and presents a
specific contribution, namely, the concept of local utilization bound, which
supports a fast and efficient schedulability analysis for on-line resource
management that assures continued safe operation. Such local bound is derived
off-line for the specific set of possible configurations, and can be
significantly higher than any generic non-necessary utilization bound such as
the well known Liu and Layland's bound for Rate-Monotonic scheduling.
[AFL07]
Composition Techniques for Tree Communication Schedules
M. Anand, S. Fischmeister, and I. Lee
A critical resource in a distributed real-time system is its shared
communication medium. Unrestrained concurrent access to the network can lead
to collisions that reduce the system's reliability. Therefore in this area,
one goal is to develop effective models for coordinating and controlling
access to the shared medium and its channels.
Network Code is a verifiable, executable model for coordinating and
controlling access to a shared communication medium in a distributed real-time
system. In this paper, we investigate the problem of building an application
by composing multiple Network Code programs. To reason about the composition,
we model Network Code programs as Tree Schedules (TS) and then consider the
composition of schedules that describe how the network is accessed by
different applications. Specifically, we first define the notions of
compatibility and composability of tree schedules, and then provide algorithms
for their composition and reason about overhead of composition. We illustrate
the techniques by considering the composition of two control applications.
[LPS07]
Resources in process algebra
Insup Lee, Anna Philippou, Oleg Sokolsky
The Algebra of Communicating Shared Resources (ACSR) is a timed
process algebra which extends classical process algebras with the
notion of a resource. It takes the view that the timing
behavior of a real-time system depends not only on delays due to
process synchronization, but also on the availability of shared
resources. Thus, ACSR employs resources as a basic primitive and
it represents a real-time system as a collection of concurrent
processes which may communicate with each other by means of
instantaneous events and compete for the usage of shared
resources. Resources are used to model physical devices such as
processors, memory modules, communication links, or any other
reusable resource of limited capacity. Additionally, they provide
a convenient abstraction mechanism for capturing a variety of
aspects of system behavior.
In this paper we give an overview of ACSR and its probabilistic
extension, PACSR, where resources can fail with associated failure
probabilities. We present associated analysis techniques for performing
qualitative analysis (such as schedulability analysis) and quantitative
analysis (such as resource utilization analysis) of process-algebraic
descriptions. We also discuss mappings between probabilistic and non-
probabilistic models, which allow us to use analysis techniques from
one algebra on models from the other.
[JFA07]
Robust Test Generation and Coverage for Hybrid Systems
A Agung Julius, Georgios E. Fainekos, Madhukar Anand, Insup Lee, and George Pappas
Testing is an important tool for validation of the system design and its implementation. Model-based test generation allows to systematically ascertain whether the system meets its design requirements, particularly the safety and correctness requirements of the system. In this paper, we develop a framework for generating tests from hybrid systems' models. The core idea of the framework is to develop a notion of robust test, where one nominal test can be guaranteed to yield the same qualitative behavior with any other test that is close to it. Our approach offers three distinct advantages: 1) It allows for computing and formally quantifying the robustness of some properties; 2) it establishes a method to quantify the test coverage for every test case; and 3) the procedure is parallelizable and therefore, very scalable. We demonstrate our framework by generating tests for a navigation benchmark application.
[MSG06]
Securing the Drop-Box Architecture for Assisted Living
Michael J. May, Wook Shin, Carl A. Gunter, and Insup Lee
Home medical devices enable individuals to monitor some of their own health information without the need for visits by nurses or trips to medical facilities. This enables more continuous information to be provided at lower cost and will lead to better healthcare outcomes. The technology depends on network communication of sensitive health data. Requirements for reliability and ease-of-use provide challenges for securing these communications. In this paper we look at protocols for the drop-box architecture, an approach to assisted living that relies on a partially-trusted Assisted Living Service Provider (ALSP). We sketch the requirements and architecture for assisted living based on this architecture and describe its communication protocols. In particular, we give a detailed description of its report and alarm transmission protocols and give an automated proof of correspondence theorems for them. Our formulation shows how to characterize the partial trust vested in the ALSP and use the existing tools to verify this partial trust.
[ABI02]
Visual Programming for Modeling and Simulation of Biomolecular Regulatory Networks
Rajeev Alur, Calin Belta, Franjo Ivancic, Vijay Kumar, Harvey Rubin, Jonathan Schug, Oleg Sokolsky, and Jonathan Webb
In this paper we introduce our new tool BIOSKETCHPAD that allows visual progamming and modeling of biological regulatory networks. The tool allows biologists to create dynamic models of networks using a menu of icons, arrows, and pop-up menus, and translates the input model into CHARON, a modeling language for modular design of interacting multi-agent hybrid systems. Hybrid systems are systems that are characterized by continuous as well as discrete dynamics. Once a CHARON model of the underlying system is generated, we are able to exploit the various analysis capabilities of the CHARON toolkit, including simulation and reachability analysis. We illustrate the advantages of this approach using a case study concerning the regulation of bioluminescence in a marine bacterium
[EKS05]
Steering of Discrete Event Systems: Control Theory Approach
Arvind Easwaran, Sampath Kannan, and Oleg Sokolsky
Runtime verification involves monitoring the system at runtime to check for conformance of the execution trace to user defined safety properties. Typically, run-time verifiers do not assume a system model and hence cannot predict violations until they occur. This limits the practical applicability of runtime verification. Steering is the process of predicting the occurrence of violations and preventing them by controlling system execution. Steerers can achieve this using a limited knowledge of the system model even in situations where it is infeasible to store the entire model. In this paper, we explore a control-theoretic view of steering for discrete event systems. We introduce an architecture for steering and also describe different steering paradigms.
[KSP06]
R-Charon, a Modeling Language for Reconfigurable Hybrid Systems
Fabian Kratz, Oleg Sokolsky, George J. Pappas, and Insup Lee
This paper describes the modeling language as an extension for architectural reconfiguration to the existing distributed hybrid system modeling language Charon. The target application domain of R-Charon includes but is not limited to modular reconfigurable robots and large-scale transportation systems. While largely leaving the Charon syntax and semantics intact, R-Charon allows dynamic creation and destruction of components (agents) as well as of links (references) between the agents. As such, R-Charon is the first formal, hybrid automata based modeling language which also addresses dynamic reconfiguration. We develop and present the syntax and operational semantics for R-Charon on three levels: behavior (modes), structure (agents) and configuration (system).
[SLC06]
Schedulability Analysis of AADL Models
Oleg Sokolsky, Insup Lee, and Duncan Clarke
The paper discusses the use of formal methods for the analysis of architectural models expressed in the modeling language AADL. AADL describes the system as a collection of interacting components. The AADL standard prescribes semantics for the thread components and rules of interaction between threads and other components in the system. We present a semantics-preserving translation of AADL models into the real-time process algebra ACSR, allowing us to perform schedulability analysis of AADL models.
[ESS06]
Incremental Schedulability Analysis of Hierarchical Real-Time Components
Arvind Easwaran, Insik Shin, Oleg Sokolsky, and Insup Lee
Embedded systems are complex as a whole but consist of smaller independent modules minimally interacting with each other. This structure makes embedded systems amenable to compositional system design. Compositional design of real-time embedded systems can be done using hierarchical systems which consist of real-time components arranged in a scheduling hierarchy. Each component consists of a real-time workload and a scheduling policy for the workload. To simplify schedulability analysis of hierarchical systems, analysis can be done compositionally using interfaces that abstract the timing requirements of components. Associative composition will facilitate analysis of systems in which components are modified on the fly. In this paper, we propose efficient algorithms to abstract the resource requirements of components in the form of periodic resource models. Each component interface consists of a set of periodic resource models for different values of period, which allows the selection of a periodic interface that minimizes the collective real-time requirements of hierarchical components. We also describe an interface composition algorithm which accounts for context switch overheads incurred by components and is associative.
[MGL06]
Privacy APIs: Access Control Techniques to Analyze and Verify Legal Privacy Policies
Michael J. May, Carl A. Gunter, and Insup Lee
There is a growing interest in establishing rules to regulate the privacy of citizens in the treatment of sensitive personal data such as medical and financial records. Such rules must be respected by software used in these sectors. The regulatory statements are somewhat informal and must be interpreted carefully in the software interface to private data. This paper describes techniques to formalize regulatory privacy rules and how to exploit this formalization to analyze the rules automatically. Our formalism, which we call privacy APIs, is an extension of access control matrix operations to include (1) operations for notification and logging and (2) constructs that ease the mapping between legal and formal language. We validate the expressive power of privacy APIs by encoding the 2000 and 2003 HIPAA consent rules in our system. This formalization is then encoded into Promela and we validate the usefulness of the formalism by using the SPIN model checker to verify properties that distinguish the two versions of HIPAA.
[AGL06]
Compositional modeling for refinement for hierarchical hybrid systems
Rajeev Alur, Radu Grosu, Insup Lee, and Oleg Sokolsky
In this paper,we develop a theory of modular design and refinement of hierarchical hybrid systems. In particular, we present compositional trace-based semantics for the language CHARON that allows modular specification of interacting hybrid systems. For hierarchical description of the system architecture, CHARON supports building complex agents via the operations of instantiation, hiding, and parallel composition. For hierarchical description of the behavior of atomic components, CHARON supports building complex modes via the operations of instantiation, scoping, and encapsulation. We develop an observational trace semantics for agents as well as for modes, and define a notion of refinement for both, based on trace inclusion. We show this semantics to be compositional with respect to the constructs in the language.
[AFL06]
An Analysis Framework for Network-Code Programs
Madhukar Anand, Sebastian Fischmeister, and Insup Lee
Distributed real-time systems require a predictable and verifiable mechanism to control the communication medium. Current real-time communication protocols are typically independent of the application and have intrinsic limitations that impede customizing or optimizing them for the application. Therefore, either the developer must adapt her application and work around these subtleties or she must limit the capabilities of the application being developed.
Network Code, in contrast, is a more expressive and flexible model that specifies real-time communication schedules as programs. By providing a programmable media access layer on the basis of TDMA, Network Code permits creating application-specific protocols that suit the particular needs of the application. However, this gain in flexibility also incurrs additional costs such as increased communication and run-time overhead. Therefore, engineering an application with network code necessitates that these costs are analyzed, quantified, and weighted against the benefits.
In this work, we propose a framework to analyze network code programs for commonly used metrics such as overhead, schedulability, and average waiting time. We introduce Timed Tree Communication Schedules, based on timed automata to model such programs and define metrics in the context of deterministic and probabilistic communication schedules. To demonstrate the utility of our framework, we study an inverted pendulum system and show that we can decrease the cumulative numeric error in the model’s implementation through analyzing and improving the schedule based on the presented metrics.
[ACS06]
Sensor Network Security: More Interesting Than You Think
Madhukar Anand, Eric Cronin, Micah Sherr, Matt Blaze,
Zachary Ives and Insup Lee
With the advent of low-power wireless sensor networks, a wealth of new applications at the interface of the real and digital worlds is emerging. A distributed computing platform that can measure properties of the real world, formulate intelligent inferences, and instrument responses, requires strong foundations in distributed computing, artificial intelligence, databases, control theory, and security.
Before these intelligent systems can be deployed in critical infrastructures such as emergency rooms and powerplants, the security properties of sensors must be fully understood. Existing wisdom has been to apply the traditional security models and techniques to sensor networks. However, sensor networks are not traditional computing devices, and as a result, existing security models and methods are ill suited. In this position paper, we take the first steps towards producing a comprehensive security model that is tailored for sensor networks. Incorporating work from Internet security, ubiquitous computing, and distributed systems, we outline security properties that must be considered when designing a secure sensor network. We propose challenges for sensor networks – security obstacles that, when overcome, will move us closer to decreasing the divide between computers and the physical world.
[ALS06]
Unit & Dynamic Typing in Hybrid Systems Modeling with CHARON
Madhukar Anand, Insup Lee, Oleg Sokolsky, and George Pappas
In scientific applications, dimensional analysis forms a basis for catching errors as it introduces a type-discipline into the equations and formulae. Dimensions in physical quantities are measured via their standard units. However, many programming and modeling tools provide limited support for incorporating these units into the variables. Thus, it is quite difficult for a programmer to ensure dimensional consistency in the code. Different existing standards for units further complicates this problem and an incautious use could cause inconsistencies, often with catastrophic results.
In this paper, we propose an extension of the basic type system in CHARON, a language for modeling of hybrid systems, to include Unit and Dynamic data types. Through a combination of indirect user-guided annotations and typeinference, we address the problem of ensuring both dimensional consistency, and consistency with respect to different unitsystems. Further, we also introduce dynamic data typing, that allows programmers to specify entities that bind at runtime. Such abstractions are particularly useful to program controllers for dynamic environments. We illustrate these benefits with an example on mobile robots.
[AKF06]
Generating Sound and Resource-Aware Code from Hybrid System Models
Madhukar Anand, Jesung Kim, Sebastian Fischmeister, and Insup Lee
Modern real-time embedded systems are complex, distributed, feature-rich applications. Model-based development of real-time embedded systems promises to simplify and accelerate the implementation process. Although there are appropriate models to design such systems and some tools that support automatic code generation from such models, several issues related to ensuring correctness of the implementation with respect to the model remain to be addressed.
In this work, we investigate how we can derive sampling rates for distributed real-time systems generated from a hybrid systems model such that there are no switching discrepancies and the resources spent in achieving this are a minimum. Of particular interest are the resulting mode switching semantics and we propose an approach to handle faulty transitions and compute execution rates for minimizing missed transitions. As a guiding example for our approach, we describe a hybrid systems model for vehicle coordination in which one vehicle acts as a leader and a second follows the leader guaranteeing to maintain a safe distance between the two vehicles.
[ADV06]
Formal Modeling and Analysis of AFDX Frame Management Design
Madhukar Anand, Samar Dajani-Brown, Steve Vestal, and Insup Lee
The Avionics Full Duplex Switched Ethernet (AFDX) has been developed to provide reliable data exchange with strong data transmission time guarantees in internal communication of the aircraft. The AFDX design is based on the principle of a switched network with physically redundant links to support availability and be tolerant to transmission and link failures in the network.
In this work, we develop a formal model of the AFDX frame management to ascertain the reliability properties of the design. To capture the precise temporal semantics, we model the system as a network of timed automata and use UPPAAL to model-check for the desired properties expressed in CTL. Our analysis indicates that the design of the AFDX frame management is vulnerable to faults such as network babbling which can trigger unwarranted system resets. We show that these problems can be alleviated by modifying the original design to include a priority queue at the receiver for storing the frames. We also suggest communicating redundant copies of the reset message to achieve tolerance to network babbling.
[LPC06]
High-Confidence Medical Device Software and Systems
Insup Lee, George J. Pappas, Rance Cleaveland, John Hatcliff, Bruce H. Krogh, Peter Lee, Harvey Rubin, and Lui Sha
Given the shortage of caregivers and the increase in an aging US population, the future of US healthcare quality does not look promising and definitely is unlikely to be cheaper. Advances in health information systems and healthcare technology offer a tremendous opportunity for improving the quality of care while reducing costs.
[SKL06]
Simulation-Based Graph Similarity
Oleg Sokolsky, Sampath Kannan, and Insup Lee
We present symmetric and asymmetric similarity measures for labeled
directed rooted graphs that are inspired by the simulation and
bisimulation
relations on labeled transition systems. Computation of the similarity
measures has close connections to discounted Markov decision processes
in
the asymmetric case and to perfect-information stochastic games in the
symmetric case. For the symmetric case, we also give a polynomial-time
algorithm that approximates the similarity to any desired precision.
[FSL06]
Network-Code Machine: Programmable Real-Time Communication Schedules
Sebastian Fischmeister, Oleg Sokolsky, and Insup Lee
Distributed hard real-time systems require guaranteed communication. One common approach is to restrict network access by enforcing a time-division multiple access (TDMA) schedule.The typical data representation of offline-generated TDMA schedules is table-like structures. This representation, however, does not permit applications with dynamic communication demands, because the table-like structure prevents on-the-fly changes during execution. A common approach for applications with dynamic communication behavior is dynamic TDMA schedules. However, such schedules are hard to verify, because they are usually implemented in a programming language, which does not support verification.
Network code is a behavioral model for specifying real-time communication schedules. It allows modeling arbitrary time-triggered communication schedules with on-the-fly choices, and it is also apt for formal verification. In this work, we present network code and show how we can use a model checker to verify safety properties such as collision-free communication, schedulability, and guaranteed message reception. We also discuss its implementation in RTLinux and provide performance measurements.
[KLC05]
End-to-end Application Performance Impact on Scheduler in CDMA-1XRTT Wireless System
Bong Ho Kim, Insup Lee, and Kelvin Chu
User-perceived application-level performance is very important to the adoption and success of 3G wireless services and infrastructure. This paper illustrates the end-to-end application performance when connecting through a CDMA-1XRTT network and compares the performance to that of a dialup connection. The results show that the application performance in CDMA-1XRTT may depend on the application traffic behavior. While many applications perform quite well in CDMA-1XRTT, others such as Microsoft Outlook perform below expectation and may even be slower than a dialup connection. This paper proposes an enhanced application sensitive scheduling algorithm to improve the performance of such applications. The enhanced algorithm also provides additional benefits for applications with similar behavior as Outlook. These include additional channel code availability and channel switching process reduction by as much as 60%.
[SLS05a]
Checking Correctness At Runtime using Real-Time Java
Usa Sammapun, Insup Lee and Oleg Sokolsky
Correctness of a real-time system depends on its computation as well as its timeliness. In recent years, research has been focusing on verifying the correctness of a real-time system during runtime by monitoring its runtime execution and checking it against its formal specifications. Such verification method is called Runtime Verification. While a few existing runtime verification tools verify both computational correctness and timeliness correctness, those that provide timeliness correctness fail to detect timeliness violations as soon as violations occur. In this paper, we investigate the verification of timeliness correctness by providing quantitative property specifications, address the problem why those tools fail to detect as soon as violations occur, provide an efficient solution, and present how to implement it in Real-Time Java.
[HLS05]
Abstract Slicing: A New Approach to Program Slicing Based on Abstract Interpretation and Model Checking
Hyoung Seok Hong, Insup Lee, and Oleg Sokolsky
This paper proposes a new approach to program slicing based on abstract interpretation and model checking. First, the notion of abstract slicing is introduced. Abstract slicing extends static slicing with predicates and constraints by using as the program model an abstract state graph, which is obtained by applying predicate abstraction to a program, rather than a flow graph. This leads to a program slice that is more precise and smaller than its static counterpart. Second, a method for performing abstract slicing is developed. It is shown that abstract slicing can be reduced to a least fixpoint computation over formulas in the branching time temporal logic CTL. This enables one to use symbolic model checkers for CTL as an efficient computation engine for abstract slicing. A prototype implementation and experimental results are reported demonstrating the feasibility of the approach.
[SLM05]
Opportunities and obligations for physical computing systems
John A. Stankovic, Insup Lee, Aloysius Mok, and Raj Rajkumar
The recent confluence of embedded and real-time systems with wireless, sensor, and networking technologies is creating a nascent infrastructure for a technical, economic, and social revolution. Based on the seamless integration of computing with the physical world via sensors and actuators, this revolution will accrue many benefits. Potentially, its impact could be similar to that of the current Internet. We believe developers must focus on the physical, real-time, and embedded aspects of pervasive computing. We refer to this domain as physical computing systems. For pervasive computing to achieve its promise, developers must create not only high-level system software and application solutions, but also low-level embedded systems solutions. To better understand physical computing's advantages, we consider three application areas: assisted living, emergency response systems for natural or man-made disasters, and protecting critical infrastructures at the national level.
[SLS05b]
RT-MaC: Runtime Monitoring and Checking of Quantitative and Probabilistic
Properties
Usa Sammapun, Insup Lee and Oleg Sokolsky
Correctness of a real-time system depends on its computation as well as its timeliness and its reliability. In recent years, researches have focused on verifying correctness of a real-time system during runtime by monitoring its execution and checking it against its formal specifications. Such verification method is called Runtime Verification. Most existing runtime verification tools verify computation correctness using qualitative property specifications but do not verify timeliness nor reliability correctness. In this paper, we investigate the verification on timeliness and reliability correctness by offering quantitative and probabilistic property specifications and implementing efficient verifiers.
[SSL05]
Run-Time Checking of Dynamic Properties
Oleg Sokolsky, Usa Sammapun, Insup Lee, and Jesung Kim
We consider a first-order property specification language for run-time monitoring of dynamic systems. The language is based on a linear-time temporal logic and offers two kinds of quantifiers to bind free variables in a formula. One kind contains the usual first-order quantifiers that provide for replication of properties for dynamically created and destroyed objects in the system. The other kind, called attribute quantifiers, is used to check dynamically changing values within the same object. We show that expressions in this language can be eficiently checked over an execution trace of a system.
[AKL05]
Code Generation from Hybrid Systems Models for Distributed Embedded Systems
Madhukar Anand, Jesung Kim, and Insup Lee
Code generation from hybrid system models is a promising
approach to producing reliable embedded systems. This approach presents new challenges as the precise semantics of the model are hard to capture in the code. A
framework for generating code was introduced for single
threaded/processor environments. Here, we extend it by
considering code generation for distributed environments. We also define criteria for faithful implementation of the
model. To this end, we define faulty and missed transitions.
For preventing faulty transitions, we build on the idea of instrumentation we have developed for sound simulation of hybrid systems. Finally, we present sufficient conditions to avoid missed transitions and provide examples.
[AFK05]
DistributedCode Generation from Hybrid Systems Models for Timedelayed
Multirate Systems
Madhukar Anand, Sebastian Fischmeister, Jesung Kim, and Insup Lee
Hybrid systems are an appropriate formalism to model embedded systems as they capture the theme of continuous dynamics with discrete control. A simple extension, a network of communicating hybrid automata, allows for modeling distributed embedded systems. Although it is possible to generate code from such models, it is difficult to provide formal guarantees in the code with respect to the model. One of the reasons for this is that, the model is set in continuous time and concurrent execution with instantaneous communication, whereas the generated code is set in discrete time with delayed communication. This can introduce semantic differences between the model and the code such as missed transitions, faulty transitions, and altered continuous behavior. The goal of faithful code generation is to minimize these differences.
In this paper, we propose a relaxed criteria of relative faithful implementation. Based on this criteria, we propose faithfulness, coined dynamically adjusting the guard at runtime using estimates of errors for preventing faulty transitions. We also identify a sufficient condition to ensure no missed transitions in the code.
[AIL05]
Quantifying Eavesdropping Vulnerability in Sensor
Madhukar Anand, Zachary G. Ives, Insup Lee
With respect to security, sensor networks have a number of considerations that separate them from traditional distributed systems. First, sensor devices are typically vulnerable to physical compromise. Second, they have significant power and processing constraints. Third, the most critical security issue is protecting the (statistically derived) aggregate output of the system, even if individual nodes may be compromised. We suggest that these considerations merit a rethinking of traditional security techniques: rather than depending on the resilience of cryptographic techniques, in this paper we develop new techniques to tolerate compromised nodes and to even mislead an adversary. We present our initial work on probabilistically quantifying the security of sensor network protocols, with respect to sensor data distributions and network topologies. Beginning with a taxonomy of attacks based on an adversary?s goals, we focus on how to evaluate the vulnerability of sensor network protocols to eavesdropping. Different topologies and aggregation functions provide different probabilistic guarantees about system security, and make different trade-offs in power and accuracy.
[SL04]
Compositional Real-Time Scheduling Framework
Insik Shin and Insup Lee
Our goal is to develop a compositional real-time scheduling framework
so that global (system-level) timing properties can be established by
composing independently (specified and) analyzed local
(component-level) timing properties. The two essential problems in
developing such a framework are (1) to abstract the collective
real-time requirements of a component as a single real-time
requirement and (2) to compose the component demand abstraction
results into the system-level real-time requirement. In our earlier
work, we addressed the problems using the Liu and Layland periodic
model. In this paper, we address the problems using another
well-known model, a bounded-delay resource partition model, as a
solution model to the problems. To extend our framework to this
model, we develop an exact feasibility condition for a set of
bounded-delay tasks over a bounded-delay resource partition. In
addition, we present simulation results to evaluate the overheads that
the component demand abstraction results incur in terms of utilization
increase. We also present new utilization bound results on a
bounded-delay resource model.
[TSL04]
Specification-based Testing with Linear Temporal Logic
Li Tan, Oleg Sokolsky, and Insup Lee
This paper considers the specification-based testing in which the
requirement is given in the linear temporal logic (LTL). The
required LTL property must hold on all the executions of the
system, which are often infinite in size and/or in length. The
central piece of our framework is a property-coverage metric. Based
on requirement mutation, the metric measures how well a property has
been tested by a test suite. We define a coverage criterion based on
the metric that selects a finite set of tests from all the possible
executions of the system. We also discuss the technique of
generating a test suite for specification testing by using the
counterexample mechanism of a model checker. By exploiting the
special structure of a generated test, we are able to reduce a test
with infinite length to an equivalent one of finite length. Our
framework provides a model-checking-assisted approach that generates
a test suite that is finite in size and in length for testing linear
temporal properties on an implementation.
[TKS04]
Model-based Testing and Monitoring for Hybrid Embedded Systems
Li Tan, Jesung Kim, Oleg Sokolsky, and Insup Lee
We propose an integrated framework for testing and monitoring the model-based embedded systems. The framework incorporates three components: 1) model-based test generation for hybrid system, 2) run-time verification, and 3) modular code generation for hybrid systems. To analyze the behavior of a model-based system, the model of the system is augmented with a testing automaton that represents a given test case, and with a monitoring automaton that captures the formally specified properties of the system. The augmented model allows us to perform the model-level validation. In the next step, we use the modular code generator to convert the testing and monitoring automata into code that can be linked with the system code to perform the validation tasks on the implementation level. The paper illustrates our techniques by a case study on the Sony AIBO robot platform.
[SP04]
Platform-Independent Autonomy Modeling
Oleg Sokolsky and George Pappas
We describe an approach for high-level modeling behaviors of autonomous
vehicles and an infrastructure for executing these behaviors on a
particular vehicle platform. The language directly represents behavioral
primitives and constraints on their composition. The control
infrastructure maps these behavioral primitives on the native vehicle
interface in a model-driven fashion. As a result, the user is presented
with an abstract motion planning interface that hides the intricate details
of the vehicle implementation.
[Sok04]
Resource Modeling for Embedded Systems Design
Oleg Sokolsky
The paper describes a formal framework for designing and
reasoning about resource-constrained embedded systems. The framework
is based on a series of process algebraic formalisms which have been previously
developed to describe and analyze various aspects of real-time
concurrent systems. We present a uniform framework for formal treatment of
resources and illustrate modeling of common resource classes.
[SLM04]
A Design Approach for Real-Time Embedded Systems with
Energy and Code Size Constraints
Insik Shin, Insup Lee, and Sang Lyul Min
Real-time embedded systems often have multiple resource constraints
such as energy and code size constraints. Traditionally, techniques
for reducing energy consumption for real-time embedded systems have
been developed without considering code size constraints, whereas
code size reduction techniques have been developed without
considering energy constraints. There, however, is a tradeoff
relationship between reducing dynamic energy consumption and
reducing code size for real-time embedded systems. Therefore,
reducing code size may result in increasing energy consumption. In
this paper, we present a triple-tradeoff relationship among code
size, execution time, and energy consumption and then address the
code size minimization problem while considering simultaneously the
energy constraints and the real-time requirements of embedded
systems. We formulate such an optimization problem and prove this
optimization problem is NP-hard. Given the difficulty of finding the
optimal solution to the problem, we then propose four heuristic
algorithms to find sub-optimal solutions and evaluate their
performance through simulations.
[KKLSV04]
Java-MaC: A Run-time Assurance Tool for Java Programs
Moonjoo Kim, Sampath Kannan, Insup Lee, Oleg Sokolsky, Mahesh Viswanathan
We describe Java-MaC, a prototype implementation of the Monitoring and Checking
(MaC) architecture for Java programs. The MaC architecture provides
assurance that the target program is running correctly with respect
to a formal requirements specification by monitoring and checking the
execution of the target program at run-time. MaC bridges the gap between
formal verification, which ensures the correctness of a design rather
than an implementation, and testing, which does not provide formal
guarantees about the correctness of the system.
Use of formal requirements specification in run-time monitoring
and checking is the salient aspect of the MaC architecture. MaC
is a lightweight formal method solution which works as a viable
complement to the current heavyweight formal methods. In additions,
analysis processes of the architecture including instrumentation
of the target program, monitoring, and checking are performed fully
automatically without human direction, which increases the accuracy
of the analysis. Another important feature of the architecture is the
clear separation between monitoring implementation-dependent low-level
behaviors and checking high-level behaviors, which allows the reuse of
a high-level requirement specification even when the target program
implementation changes. Furthermore, this seperation makes the
architecture modular and allows the flexibility of incorporating third
party tools into the architecture. The paper presents an overview
of the MaC architecture and a prototype implementation Java-MaC.
[SELS04]
Simulation of Simultaneous Events in Regular Expressions for Run-Time Verification
Usa Sammapun, Arvind Easwaran, Insup Lee, Oleg Sokolsky
When specifying system requirements, we want a language that can
express the requirements in the simplest and most intuitive form.
Although the MaC system provides an expressive language, called MEDL,
it is generally awkward to express certain features like temporal
ordering of complex events, timing constraints, and frequencies of
events which are inherent in safety properties. MEDL-RE extends the
MEDL language to include regular expressions to easily specify timing
dependencies and timing constraints. Due to simultaneous events
generated by the MaC system, monitoring regular expressions by
simulating DFAs would result in a potential problem. The DFA
simulations would involve concurrent multi-path simulations and result
in exponential running time. To handle simultaneous events
inexpensively, we generate a dependency graph to identify possible
simultaneous events. Further, we augment the original DFAs with
alternative transitions, which will substitute for multi-path simulations.
[AAG04]
Formal specifications and analysis of the computer-assisted resuscitation
algorithm (CARA) Infusion Pump Control System
Rajeev Alur, David Arney,
Elsa L. Gunter, Insup Lee, Jaime Lee, Wonhong Nam, Frederick Pearce, Steve
Van Albert, Jiaxiang Zhou
Reliability of medical devices such as the CARA Infusion Pump Control System
is of extreme importance given that these devices are being used on
patients in critical condition. The Infusion Pump Control System includes
embedded processors and accompanying embedded software for monitoring
as well as controlling sensors and actuators that allow the embedded
systems to interact with their environments. This nature of the
Infusion Pump Control System adds to the complexity of assuring the
reliability of the total system. The traditional methods of
developing embedded systems are inadequate for such safety-critical
devices. In this paper, we study the application of formal methods to
the requirements capture and analysis for the Infusion Pump Control System.
Our approach consists of two phases. The first phase is to convert
the informal design requirements into a set of reference
specifications using a formal system, in this case EFSMs (Extended
Finite State Machines). The second phase is to translate the reference
specifications to the tools supporting formal analysis, such as SCR and Hermes.
This allows us to conclude properties of the reference specifications.
Our research goal is to develop a framework and methodology for the
integrated use of formal methods in the development of embedded
medical systems that require high assurance and confidence.
[HSCC04]
Sound Code Generation from Communicating Hybrid Models
Yerang Hur, Jesung Kim, Insup Lee, and Jin-Young Choi
Precise translation from hybrid models to code is difficult because models are
defined in the continuous-time domain whereas code executes on digital
computers in a discrete fashion. Traditional approach is to associate the
model with a sampling rate before code generation, and rely on an approximate
algorithm that computes the next state numerically. Depending on the choice
of the sampling rate and the algorithm, the behavior of the code may vary
significantly due to numerical errors, but the discrepancy has been addressed
informally, making the analysis results at the model level less meaningful for
implementation. Formal relationship between the model and the code becomes
even more unclear when components of the code execute concurrently.
In this paper, we propose a formal framework that addressesthe issue of
soundness of concurrent programs generated from communicating hybrid models.
The motivation is that concurrent programs executing in different rates may
cause an erroneous transition when transition conditions are evaluated using
values from different time instances. The essence of our technique is to
refine the model by tightening transition conditions according to the maximum
errors due to different sampling rates. We claim that the generated code has a
trace of discrete transitions that is equivalent to one of the traces observable
from the model, and that the values of variables are bounded. Our framework
demonstrates how hybrid models defined in the continuous time domain are
translated into discretized models with or without consideration of errors due
to asynchronous sampling, and finally into executable code with real-time
scheduling.
[SS03]
Regular Expressions for Run-Time Verification
Usa Sammapun, Oleg Sokolsky
When specifying system requirements, we want a language that can express
the requirements in the simplest and most intuitive form.
An expressive and intuitive language makes specifying requirements easier
and less error-prone. Although our MaC system provides an expressive
language, called MEDL, to specify safety requirements, it is
generally awkward to express an order of events with complex
timing dependencies, timing constraints, and frequencies of events.
MEDL-RE extends our MEDL language to include regular expression
and three associated events to easily specify timing dependencies
and its timing constraints. Our regular expression is unique in
a way that a user can specify which events are relevant to a regular
expression. This feature makes it easy when a user wants to specify
a requirement of one specific component of a system.
[RTSS03]
Periodic Resource Model for Compositional Real-Time Guarantees
Insik Shin and Insup Lee
We address the problem of providing compositional hard real-time guarantees
in a hierarchy of schedulers.
We first propose a resource model to characterize a periodic resource
allocation and present exact schedulability conditions for our
proposed resource model under the EDF and RM algorithms.
Using the exact schedulability conditions,
we then provide methods to abstract the timing requirements that a set
of periodic tasks demands under the EDF and RM algorithms as a single
periodic task. With these abstraction methods,
for a hierarchy of schedulers,
we introduce a composition method that derives the timing requirements
of a parent scheduler from
the timing requirements of its child schedulers
in a compositional manner
such that the timing requirement of the parent scheduler is satisfied,
if and only if, the timing requirements of
its child schedulers are satisfied.
[TKL03]
Testing and Monitoring Model-based Generated Program
Li Tan, Jesung Kim, and Insup Lee
We propose an integrated framework to test and monitor code generated
from hybrid models for embedded systems. The framework consists of the
following elements: First, we create testing automata as a controlled
environment to produce test traces achieving the desired testing criteria;
Second, we synthesize monitoring automata from the behavior specification
to check the run-time behavior of the tested system in response to the test
traces; Finally, since both automata are encoded in the same language as the
system model, the same code generator may be used to generate a tester and
a monitor from the testing automata and the monitoring automata, and link
them with the code generated from the system model. Our approach yields
self-testing and self-monitoring code which may be run both on the simulation
level and on the code level. We discuss our approach in its full details
through an example on a SONY AIBO robotic dog.
[LCTES03]
Generating Embedded Software from Hierarchical Hybrid Models
Franjo Ivancic, Jesung Kim, Insup Lee and Oleg Sokolsky
Benefits of high-level modeling and analysis are significantly
enhanced if code can be generated automatically
from a model such that the correspondence between the
model and the code is precisely understood. For embedded
control software, hybrid systems is an appropriate
modeling paradigm because it can be used to specify
continuous dynamics as well as discrete switching between
modes. Establishing a formal relationship between
the mathematical semantics of a hybrid model
and the actual executions of the corresponding code is
particularly challenging due to sampling and switching
errors. In this paper, we describe an approach to compile
the modeling language Charon that allows hierarchical
specifcations of interacting hybrid systems. We
show how to exploit the semantics of Charon to generate
code from a model in a modular fashion, and identify
sufficient conditions on the model that guarantee the
absence of switching errors in the compiled code. The
approach is illustrated by compiling a model for coordinated
motion of legs for walking onto Sony's AIBO
robot.
[RTAS03]
Modular Code Generation from Hybrid Automata based on Data Dependency
Jesung Kim and Insup Lee
Model-based automatic code generation is a process
of converting abstract models into concrete implementations
in the form of a program written in a high-level
programming language. The process consists of two
steps, first translating the primitives of the model into
(approximately) equivalent implementations, and then
scheduling the implementations of primitives according
to the data dependency inherent in the model. When
the model is based on hybrid automata that combine
continuous dynamics with a finite state machine, the
data dependency must be viewed in two aspects: continuous
and discrete. Continuous data dependency is
present between mathematical equations modeling timecontinuous
behavior of the system. On the other hand,
discrete data dependency is present between guarded
transitions that instantaneously change the continuous
behavior of the system. While discrete data dependency
has been studied in the context of code generation from
modeling languages with synchronous semantics (e.g.,
ESTEREL), there has been no prior work that addresses
both kinds of dependency in a single framework. In this
paper, we propose a code generation framework for hybrid
automata which deals with continuous and discrete
data dependency. We also propose techniques for generating
modular code that retains modularity of the original
model. The framework has been implemented based
on the hybrid system modeling language CHARON, and
experimented with Sony's robot platform AIBO.
[HC03]
Data Flow Testing as Model CheckingHyoung Seok Hong, Sung Deok Cha, Insup Lee, Oleg Sokolsky, and Hasan
Ural
This paper presents a model checking-based approach to data flow testing. We
characterize data flow oriented coverage criteria in temporal logic such that
the problem of test generation is reduced to the problem of finding witnesses
for a set of temporal logic formulas. The capability of model checkers to
construct witnesses and counterexamples allows test generation to be fully
automatic. We discuss complexity issues in minimal cost test generation and
describe heurstic test generation algorithms. We illustrate our approach using
CTL as temporal logic and SMV as model checker.
[SPL03]
Modeling and Analysis of Power-Aware Systems
Oleg Sokolsky, Anna Philippou, Insup Lee, and Kyriakos Christou
The paper describes a formal approach for designing and reasoning about power-constrained, timed systems. The framework is based on process algebra, a formalism that has been developed to describe and analyze communicating concurrent systems. The proposed extension allows the modeling of probabilistic resource failures, priorities of resource usages, and power consumption by resources within the same formalism. Thus, it is possible to model alternative power-consumption behaviors and analyze tradeoffs in their timing and other characteristics. This paper describes the modeling and analysis techniques, and illustrates them with examples, including a dynamic voltage-scaling algorithm.
[ADE03]
Hierarchical Modeling and Analysis of Embedded Systems
Rajeev Alur, Thao Dang, Joel Esposito, Yerang Hur, Franjo Ivancic, Vijay Kumar,
Insup Lee, Pradyumna Mishra, George Pappas, and Oleg Sokolsky
This paper describes the modeling language CHARON for modular design of interacting hybrid systems. The language allows specification of architectural as well as behavioral hierarchy, and discrete as well as continuous activities. The modular structure of the language is not merely syntactic, but is exploited by analysis tools, and is supported by a formal semantics with an accompanying compositional theory of refinement. We illustrate the benefits of CHARON in design of embedded control software using examples from automated highways concerning vehicle coordination.
[LPS02a]
Process Algebraic Modeling and Analysis of Power-Aware Real-Time Systems
Insup Lee, Anna Philippou, Oleg Sokolsky
The paper describes a unified formal framework for designing and reasoning about
power-constrained, real-time systems. The framework is based on process algebra,
a formalism which has been developed to describe and analyze communicating,
concurrent systems. The proposed extension allows the modeling of probabilistic
resource failures, priorities of resource usages, and power consumption by
resources within the same formalism. Thus, it is possible to evaluate
alternative power-consumption behaviors and tradeoffs under different real-time
schedulers, resource limitations, resource failure probabilities, etc. This
paper describes the modeling and analysis techniques, and illustrates them with
examples, including a dynamic voltage-scaling algorithm.
[SLM02]
Embedded System Design Framework for Minimizing Code Size and Guaranteeing Real-Time Requirements
Insik Shin, Insup Lee, Sang Lyul Min
In addition to real-time requirements, the program code size is a critical design factor for real-time embedded systems. To take advantage of the code size vs. execution time tradeoff provided by reduced bit-width instructions, we propose a design framework that transforms the system constraints into task parameters guaranteeing a set of requirements. The goal of our design framework is to derive the temporal parameters and the code size parameter of each task in such a way that they collectively guarantee the system end-to-end timing requirements while the system code size is minimized. Our design framework is based on asynchronous periodic tasks with pre-period deadlines under EDF scheduling. For schedulability analysis, we present a new feasibility condition that can be more efficiently evaluated than existing ones.
When the code size vs. execution time tradeoff can be safely approximated as linear functions, the minimization problem becomes a linear programming problem. However, when the tradeoff is given by a table of possible (code size, execution time) pairs, the problem becomes NP-hard. We provide three heuristic algorithms that can find sub-optimal solutions and evaluate their performance with simulation results.
[LPS02b]
A General Resource Framework for Real-Time Systems
Insup Lee, Anna Philippou, and Oleg Sokolsky
The paper describes a formal framework for designing and reasoning about
resource-constrained systems. The framework is based on a series of process
algebraic formalisms which have been previously developed to describe and
analyze various aspects of real-time communicating, concurrent systems. We
develop a uniform framework for formal treatment of resources and demonstrate
how previous work fits into the new framework.
[KKL02]
Computational Analysis of Run-time Monitoring - Fundamentals of Java-MaC
Moonjoo Kim, Sampath Kannan, Insup Lee, Oleg Sokolsky, Mahesh Viswanathan
A run-time monitor shares computational resources, such as memory and CPU time,
with the target program. Furthermore, heavy computation performed by a monitor
for checking target program's execution with respect to requirement properties
can be a bottleneck to the target program's execution. Therefore, computational characteristics
of run-time monitoring cause a significant impact on the target program's
execution. We investigate computational issues on run-time monitoring. The
first issue is the power of run-time monitoring. In other words, we study the
class of properties run-time monitoring can evaluate. The second issue is
computational complexity of evaluating properties written in process algebraic
language. Third, we discuss sound abstraction of the target program's execution,
which does not change the result of property evaluation. This abstraction can be
used as a technique to reduce monitoring overhead. Theoretical understanding
obtained from these issues affects the implementation of Java-MaC, a toolset for
the run-time monitoring and checking of Java programs. Finally, we demonstrate
the abstraction-based overhead reduction technique implemented in Java-MaC
through a case study.
[KLS02]
Monitoring, Checking, and Steering of Real-Time Systems
Moonjoo Kim, Insup Lee, Usa Sammapun, Jangwoo Shin, Oleg Sokolsky
The MaC system has been developed to provide assurance that a target program is running correctly with respect to formal requirements
specification. This is achieved by monitoring and checking the execution of the target program at run-time. MaC bridges the gap
between formal verification, which ensures the correctness of a design rather than an implementation, and testing, which only partially
validates an implementation. One weakness of the MaC system is that it can detect property violations but cannot provide any feedback to
the running system. To remedy this weakness, the MaC system has been extended with a feedback capability. The resulting system is called
MaCS (Monitoring and Checking with Steering). The feedback component uses the information collected during monitoring and checking to
steer the application back to a safe state after an error occurs. We present a case study where MaCS is used in a control system that
keeps an inverted pendulum upright. MaCS detects faults in controllers and performs dynamic reconfiguration of the control system
using steering.
[HL02]
Distributed Simulation of Multi-Agent Hybrid Systems
Yerang Hur and Insup Lee
Systems such as coordinating robot systems, automobiles, aircrafts, and chemical process control systems can be modeled
as interacting hybrid systems, where hybrid systems are finite state machines with continuous dynamics.
The language CHARON and its simulator have been developed to model and analyze interacting hybrid systems as communicating
agents.
Simulations are widely used for the analyses of hybrid systems. The simulation of a complex system is, however, usually very slow.
This paper proposes four algorithms for distributed simulations of hybrid systems. The idea behind distributed simulations is
to achieve a speedup by utilizing multiple computing resources. The agents of a modeled system are distributed over multiple processors
to simulate the agents more efficiently. Since the state of the agent is affected by the input from
other agents, they synchronize to update their local states. The challenge here is how to reduce the agent synchronization overhead.
We present two approaches for resolving the problem: conservative and optimistic approaches.
For the optimistic approach, we present three different algorithms for distributed simulations of hybrid systems,
and compare them.
[HLS02]
A Temporal Logic Based Theory of Test Coverage and Generation
Hyoung Seok Hong,
Insup Lee, Oleg Sokolsky, and Hasan Ural
This paper presents a theory of test coverage and generation from specifications written in extended finite state machines
(EFSMs). We investigate a family of coverage criteria based on the information of control flow and data flow in EFSMs and
characterize them using the temporal logic CTL. We discuss the complexity of minimal cost test generation and
describe a simple heuristic which uses the capability of model checkers to construct counterexamples.
Our approach extends the range of applications of model checking from automatic verification of finite state systems
to automatic test generation from finite state systems.
[BGK02]
Verisim: Formal Analysis of Network Simulations
Karthikeyan Bhargavan, Carl A. Gunter, Moonjoo Kim, Insup Lee,
Davor Obradovic, Oleg Sokolsky, and Mahesh Viswanathan
Network protocols are often analyzed using simulations. We demonstrate how to extend such simulations to check propositions expressing safety properties of network event traces in an extended form of linear temporal logic. Our technique uses the NS simulator together with a component of the MaC system to provide a uniform framework. We demonstrate its effectiveness by analyzing simulations of the Ad Hoc On-Demand Distance Vector
(AODV) routing protocol for packet radio networks. Our analysis finds violations of significant properties, and we discuss the faults that cause them. Novel aspects of our approach include modest integration costs with other simulation objectives such as performance evaluation, greatly increased flexibility in specifying properties to be checked, and techniques for analyzing complex traces of alarms raised by the monitoring software.
[AKL01]
Fair Real-time Traffic Scheduling over A Wireless LAN
Maria Adamou, Sanjeev Khanna, Insup Lee, Insik Shin, Shiyu Zhou
Unpredictable wireless channel errors may cause applications with real-time traffic to receive degraded quality of services due to packet
losses. In the presence of such errors, a challenging problem is how to schedule packets to achieve fairness among real-time flows and to maximize
the overall system throughput simultaneously. We capture fairness by minimizing the maximum degradation in service over all flows. In this paper, we show that no online algorithm can guarantee a bounded
performance ratio with respect to the optimal algorithm. We then compare four different online algorithms and evaluate them using simulations. The
first two are EDF (Earliest Deadline First) and GDF (Greatest Degradation First) that consider only one aspect of our scheduling goal respectively.
EDF is naturally suited for maximizing throughput while GDF seeks to minimize the maximum degradation. The next two are algorithms, called EOG
(EDF or GDF) and LFF (Lagging Flows First), that consider the two aspects of our scheduling goal. EOG simply combines EDF and GDF, whereas LFF tries
To favor lagging flows in a non-trivial manner. Our simulation results show that LFF is almost as good as EDF in maximizing the throughput and also is
better than GDF in minimizing the maximum degradation. Finally, we also show that there is an optimal polynomial time algorithm for the offline
version of the problem.
[LPS01]
Formal Modeling and Analysis of Power-Aware Real-Time Systems
Insup Lee, Anna Philippou, and Oleg Sokolsky
The paper describes a unified formal framework for designing and reasoning about power-constrained, timed systems. The framework is based on process algebra, a formalism which has been developed to describe and analyze communicating, concurrent systems. The proposed extension allows the modeling of probilistic resource failures and power consumption by resources within the same formalism. Thus, it is possible to study several alternative power-consumption behaviors and tradeoffs in their timing and other characteristics. This paper describes the modeling and analysis techniques, and illustrates them with examples, including a power-aware ad-hoc network protocol.
[LCK01]
A Family of Resource-Bound Real-time Process Algebras
Insup Lee, Jin-Young Choi, Hee-Hwan Kwak, Anna Philippou, and Oleg Sokolsky
This paper describes three real-time process algebras, ACSR, PACSR and ACSR-VP. ACSR is a resource-bound
real-time process that supports synchronous timed actions and asynchronous instantaneous events as well as
the notions of resource, priority, exception, and interrupt. PACSR is a probabilistic extension of ACSR with
resources that can fail and associated failure probabilities. ACSR-VP extends ACSR with value passing between
processes and parameterized process definitions. This paper also provides three simple real-time system
examples to illustrate the expressive power and analysis technique of each process algebra.
[KKL01]
Java-MaC: a Run-time Assurance Tool for Java
Moonjoo Kim, Sampath Kannan, Insup Lee, Oleg Sokolsky
We describe Java-MaC, a prototype implementation of the Monitoring and Checking
(MaC) architecture for Java
programs. The MaC architecture provides assurance about the correct execution of target programs at run-time.
Monitoring and checking is performed based on a formal specification of system requirements. MaC bridges the gap
between formal verification, which ensures the correctness of a design rather than an implementation, and testing,
which only partially validates an implementation. Java-MaC provides a practical, lightweight, formal method
solution as a viable complement to the current heavyweight formal methods. An important aspect of the architecture
is the clear separation between monitoring implementationdependent low-level activities and checking high-level
activities against a formal requirements specification. Another salient feature is automatic instrumentation of
executable codes. The paper presents an overview of the MaC architecture and a prototype implementation
Java-MaC.
[PSL01]
Hiding Resources that Can Fail
Anna Philippou, Oleg Sokolsky, Insup Lee, Rance Cleaveland, and Scott Smolka
In earlier work, we presented a process algebra, PACSR, that uses resource failures to capture probabilistic behavior in reactive systems. In
this paper, we explore the effects of resource failures in the situation where resources may be hidden from the environment. For this purpose, we introduce
a subset of PACSR, called "PACSR-lite,'' that allows us to isolate the issues surrounding resource hiding, and we provide a sound and complete
axiomatization of strong bisimulation for this fragment.
[ADE01]
Hierarchical Hybrid Modeling of Embedded Systems
Rajeev Alur, Thao Dang, Joel Esposito, R. Fierro, Yerang Hur, Franjo Ivancic, Vijay Kumar,
Insup Lee, Pradyumna Mishra, George Pappas, and Oleg Sokolsky
This paper describes the modeling language CHARON for modular design of interacting hybrid systems. The language allows specification of architectural
as well as behavioral hierarchy, and discrete as well as continuous activities. The modular structure of the language is not merely syntactic,
but is exploited by analysis tools, and is supported by a formal semantics
with an accompanying compositional theory of refinement. We illustrate the
benefits of CHARON in design of embedded control software using examples from automated highways concerning vehicle coordination.
[SL01]
Characterizing Non-Zenoness on Real-Time Processes
Jitka Stribrna and Insup Lee
In this paper we examine an important property of correct system design that is called
non-Zenoness or time progress. We present a method that allows to check non-Zenoness on a restricted
subclass of real-time processes. The processes that we examine are constructed by nondeterministic sum and parallel composition with
synchronization. The method is based on the construction of a finite representation of the potentially infinite state space of a process,
that preserves time progress.
[HLSC01]
Automatic Test Generation from Statecharts Using Model Checking
Hyoung Seok Hong, Insup Lee, Oleg Sokolsky, and Sung Deok Сha
This paper discusses the application of model checking to test generation from
statecharts. We consider a family of coverage criteria based on the control
flow and data flow of statecharts and formulate the problem of test generation
as finding counterexamples during the model checking of statecharts. The
ability of model checkers to construct counterexamples allows test generation
to be automatic.
To illustrate our approach, we use the temporal logic CTL and its symbolic
model checker SMV. We describe how to translate statecharts to inputs to SMV
after defining the semantics of statecharts in terms of Kripke structures. We,
then, describe how to express various coverage criteria in CTL and show how SMV
can be used to generate only executable tests.
[SH01]
Qualitative Modeling of Hybrid Systems
Oleg Sokolsky and Hyoung Seok Hong
The paper discusses an approach to construct discrete abstractions of hybrid
systems by means of qualitative reasoning. The work is performed in the
context of a modeling language for hybrid systems CHARON. We introduce a
qualitative version of the language and describe the abstraction technique
using a motivational example. The resulting abstract model is conservative and
can be used to analyze properties of the original hybrid system.
[AGL01]
Compositional Refinement for Hierarchical Hybrid Systems
Rajeev Alur, Radu Grosu, Insup Lee, and Oleg Sokolsky
In this paper, we develop a theory of modular design and refinement of hierarchical hybrid systems.
In particular, we present compositional trace-based semantics for the language CHARON that allows modular specification of interacting
hybrid systems.
For hierarchical description of the system architecture, CHARON supports building complex agents via the operations of instantiation,
hiding, and parallel composition.
For hierarchical description of the behavior of atomic components, CHARON supports building complex modes via the operations of instantiation,
scoping, and encapsulation.
We develop an observational trace semantics for agents as well as for modes, and define a notion of refinement for both, based on trace inclusion.
We show this semantics to be compositional with respect to the constructs in the language.
[AGH00]
Modular specifications of hybrid systems in CHARON
Rajeev Alur, Radu Grosu, Yerang Hur, Vijay Kumar, and Insup Lee
We propose a language, called CHARON, for modular specification of interacting hybrid systems.
For hierarchical description of the system architecture, CHARON supports building complex agents via the operations of instantiation,
hiding, and parallel composition. For hierarchical description of the behavior of atomic components,
CHARON supports building complex modes via the operations of instantiation,
scoping, and encapsulation. Features such as weak preemption, history retention, and externally
defined Java functions, facilitate the description of complex discrete behavior.
Continuous behavior can be specified using differential as well as algebraic constraints, and invariants restricting the flow spaces,
all of which can be declared at various levels of the hierarchy. The modular structure of the language is not merely syntactic, but
can be exploited during analysis. We illustrate this aspect by presenting a scheme for modular simulation
in which each mode can be compiled solely based on the locally declared information to execute its discrete and continuous updates, and furthermore,
submodes can integrate at a finer time scale than the enclosing modes.
[ADE00]
A framework and architecture for multirobot coordination
Rajeev Alur, A. Das, Joel Esposito, R. Fierro, Yerang Hur, G. Grudic, Vijay Kumar,
Insup Lee, J. Ostrowski, George Pappas, J. Southall, J. Spletzer, and C. Taylor
In this paper, we present a framework and the software architecture for the deployment of multiple autonomous
robots in an unstructured and unknown environment with applications ranging from scouting and reconnaissance, to search
and rescue and manipulation tasks. Our software framework provides the methodology and the tools that enable robots to exhibit
deliberative and reactive behaviors in autonomous operation, to be reprogrammed by a human operator at run-time, and to learn and
adapt to unstructured, dynamic environments and new tasks, while providing performance guarantees. We demonstrate the algorithms
and software on an experimental testbed that involves a team of car-like robots using a single omnidirectional camera as a sensor
without explicit use of odometry.
[PLS00]
Weak Bisimulation for Probabilistic Systems
Anna Philippou, Insup Lee, and Oleg Sokolsky
In this paper, we introduce weak bisimulation in the framework of Labeled Concurrent Markov Chains, that is, probabilistic
transition systems which exhibit both probabilistic and nondeterministic behavior. By resolving the nondeterminism present, these models can be
decomposed into a possibly infinite number of computation trees. We show that in order to compute weak bisimulation it is sufficient to restrict
attention to only a finite number of these computations. Finally, we present an algorithm for deciding weak bisimulation which has
polynomial-time complexity in the number of states of the transition system.
[BGK00]
Verisim: Formal Analysis of Network Simulations
Karthikeyan Bhargavan, Carl A. Gunter, Moonjoo Kim, Insup Lee,
Davor Obradovic, Oleg Sokolsky, Mahesh Viswanathan
Network protocols are often analyzed using simulations. We demonstrate how to
extend such simulations to check propositions expressing safety properties of
network event traces in an extended form of linear temporal logic. Our
technique uses the NS/2 simulator together with the Penn Monitoring and
Checking (MaC) system to provide a uniform framework. We demonstrate its
effectiveness by analyzing simulations of the Ad-Hoc On-demand Distance Vector
(AODV) routing protocol for packet radio networks. Our analysis finds
violations of significant properties and we discuss the faults that cause them.
Novel aspects of our approach include modest integration costs with other
simulation objectives such as performance evaluation, greatly increased
flexibility in specifying properties to be checked, and techniques for
analyzing complex traces of alarms raised by the monitoring software.
[BLS99]
Specification and Analysis of Real-Time Systems with PARAGON
Hanêne Ben-Abdallah, Insup Lee, and Oleg Sokolsky
This paper describes a methodology for the specification and analysis of
distributed real-time systems using the toolset called PARAGON. PARAGON is
based on the Communicating Shared Resources paradigm, which allows a
real-time system to be modeled as a set of communicating processes that compete
for shared resources. PARAGON supports both visual and textual
languages for describing real-time systems. It offers automatic
analysis based on state space exploration as well as user-directed simulation.
Our experience with using PARAGON in several case studies resulted in a
methodology that includes design patterns and abstraction heuristics, as well
as an overall process. This paper briefly overviews the communicating shared
resource paradigm and its toolset PARAGON, including the textual and visual
specification languages. The paper then describes our methodology with special
emphasis on heuristics that can be used in PARAGON to reduce the state space.
To illustrate the methodology, we use examples from a real-life system case
study.
[GSL99]
Distributed Spatial Control and Global Monitoring of Mobile Agents
Diana Gordon, William Spears, Insup Lee and Oleg Sokolsky
In this paper, we combine two frameworks in the context of an important application. The first framework, called "artificial physics", is described in detail in a companion paper by Spears and Gordon (1999). The purpose of artificial physics is the distributed spatial control of large collections of mobile physical agents. The agents can be composed into geometric patterns (e.g., to act as a sensing grid) by having them sense and respond to local artificial forces that are motivated by natural physics laws. The purpose of the second framework is global monitoring of the agent formations developed with artificial physics. Using only limited global information, the monitor checks that the desired geometric pattern emerges over time as expected. If there is a problem, the global monitor steers the agents to self-repair. Our combined approach of local control through artificial physics, global monitoring, and "steering" for self-repair is implemented and tested on a problem where multiple agents from a hexagonal lattice pattern.
[AEK99]
Formal modeling and analysis of hybrid systems: A case study in multi-robot
coordination
Rajeev Alur, Joel Esposito, Moonjoo Kim, Vijay Kumar and Insup Lee
The design of controllers for hybrid systems (i.e. mixed discrete continuous systems) in a systematic manner remains a challenging
task. In this case study, we apply formal modeling to the design of
communication and control strategies for a team of autonomous robots to
attain specified goals in a coordinated manner. The model of linear hybrid
automata is used to describe the high-level design, and the verification software HyTech is used for symbolic analysis of the description. The goal
of the project is to understand tradeoffs among various design alternatives
by generating constraints among parameters using symbolic analysis. In this
paper, we report on difficulties in modeling a team of robots using linear
hybrid automata, results of analysis experiments, promise of the approach,
and challenges for future research.
[LKK99]
Runtime Assurance Based On Formal Specifications
Insup Lee, Sampath Kannan, Moonjoo Kim, Oleg Sokolsky and Mahesh Viswanathan
We describe the Monitoring and Checking framework that assures the
correctness of the current execution at run-time. Monitoring is
performed based on a formal specification of system requirements. Our
framework bridges the gap between formal verification and testing.
The former is used to ensure the correctness of a design specification
rather than an implementation, whereas the latter is to used to
validate partially an implementation. An important aspect of the
framework is clear separation between implementation-dependent
description of monitored objects and high-level requirements
specification. Another salient feature is automatic instrumentation
of executable code. The paper presents an overview of the framework
and two languages for specifying events and conditions and their
three-value logic semantics. These two languages are used to specify
what to observe in the program and the requirements that the program
must satisfy, respectively. The paper also briefly describes our
current prototype implementation in Java.
[KVL99]
Formally Specified Monitoring of Temporal Properties
Moonjoo Kim, Mahesh Viswanathan, Insup Lee, Hanêne Ben-Abdellah, Sampath
Kannan, and Oleg Sokolsky
We describe the Monitoring and Checking (MaC) framework which provides
assurance on the correctness of an execution of a real-time system at run-time.
Monitoring is performed based on a formal specification of system requirements.
MaC bridges the gap between formal specification, which analyzes designs rather
than implementations, and testing, which validates implementations but lacks
formality. An important aspect of the framework is a clear separation
between implementation-dependent description of monitored objects and
high-level requirements specification. Another salient feature is automatic
instrumentation of executable code.
The paper presents an overview of the framework, languages to express
monitoring scripts and requirements, and a prototype implementation of MaC
targeted at systems implemented in Java.
[BCC98]
A Process Algebraic Approach to the Schedulability Analysis of Real-Time Systems
Hanêne Ben-Abdallah, Jin-Young Choi,
Duncan Clarke, Young Si Kim, Insup Lee and Hong-Liang Xie
To engineer reliable real-time systems, it is desirable to detect
timing anomalies early in the development process. However, there
is little work addressing the problem of accurately predicting
timing properties of real-time systems before implementations are
developed. This paper describes an approach to the specification
and schedulability analysis of real-time systems based on the timed
process algebra ACSR-VP, which is an extension of ACSR with value-passing
communication and dynamic priorities. Combined with the existing features
of ACSR for representing time, synchronization and resource requirements,
ACSR-VP is capable of specifying a variety of real-time systems with
different scheduling disciplines in a modular fashion. Moreover, we
can use VERSA, a toolkit we have developed for ACSR, to
perform schedulability analysis on real-time systems specified in
ACSR-VP automatically by checking for a certain bisimulation relation.
[BeLe98]
A Graphical Language with Formal Semantics for the
Specification and Analysis of Real-Time Systems
Hanêne Ben-Abdallah and Insup Lee
We present Graphical Communicating Shared Resources, GCSR, a formal
language for the specification and analysis of real-time systems,
including their functional, temporal and resource requirements.
GCSR supports the explicit representation of system resources and
priorities to arbitrate resource contentions. These features allow
a designer to examine resource inherent constraints and to
experiment with various resource allocations and scheduling
disciplines in order to produce a more dependable specification.
In addition, GCSR differs from other graphical languages through
its well-defined notions of modularity and hierarchy: dependencies
between system components, expressed as communication events, can
have a limited scope of visibility, and control flow between
components is clearly represented as either an interrupt or
exception, i.e., voluntary release of control. Furthermore, GCSR
has a precise operational semantics and notions of equivalence that
allow the execution and formal analysis of a specification. We
present the GCSR language, its toolset, and how properties, e.g.,
safety can be analyzed within GCSR.
[KLP98]
Symbolic Schedulability Analysis of Real-time Systems
Hee-Hwan Kwak, Insup Lee, Anna Philippou, Jin-Young Choi, and Oleg Sokolsky
We propose a unifying method for analysis of scheduling problems in real-time
systems. The method is based on ACSR-VP, a real-time process algebra with
value-passing capabilities. We use ACSR-VP to describe an instance of a
scheduling problem as a process that has parameters of the problem as free
variables. The specification is analyzed by means of a symbolic algorithm.
The outcome of the analysis is a set of equations, a solution to which yields
the values of the parameters that make the system schedulable. Equations are
solved using integer programming or constraint logic programming. The paper
presents specifications of two scheduling problems as examples.
[KLS98]
Parametric Approach to the Specification and Analysis of Real-time System Designs based on ACSR-VP
Hee-Hwan Kwak, Insup Lee, and Oleg Sokolsky
To engineer reliable real-time systems, it is desirable to discover
timing anomalies early in the development process. However, there is
little work addressing the problem of accurately predicting timing
properties of real-time systems before implementations are developed.
This paper describes an approach to the specification and analysis of
scheduling problems of real-time systems. The method is based on
ACSR-VP, which is an extension of ACSR, a real-time process algebra,
with value-passing capabilities. Combined with the existing features
of ACSR for representing time, synchronization and resource
requirements, ACSR-VP can be used to describe an instance of a
scheduling problem as a process that has parameters of the problem as
free variables. The specification is analyzed by means of a symbolic
algorithm. The outcome of the analysis is a set of equations and a
solution to which yields the values of the parameters that make the
system schedulable. These equations can be solved using integer
programming or constraint logic programming. The paper presents the
theory of ACSR-VP briefly and an example of the period assignment
problem for rate-monotonic scheduling. We also explain our current
tool implementation effort and plan for incorporating it into the
existing toolset, PARAGON.
[LBK98]
A Monitoring and Checking Framework for Run-time Correctness Assurance
Insup Lee, Hanêne Ben-Abdallah, Sampath Kannan, Moonjoo Kim,
Oleg Sokolsky and Mahesh Viswanathan
Computer systems are often monitored for performance evaluation and
enhancement, debugging and testing, control or to check for the
correctness of the system. Recently, the problem of designing
monitors to check for the correctness of system implementation has
received increased attention from the research community.
Traditionally, verification has been used to increase the confidence
that a system will be correct by making sure that a design
specification is correct. However, even if a design has been formally
verified, it still does not ensure the correctness of an
implementation of the design. This is because the implementation
often is much more detailed, and may not strictly follow the formal
design. So, there is possibility for introduction of errors into an
implementation of a design that has been verified. One way that
people have traditionally tried to overcome this gap between the
design and the implementation has been to test the implementation's
behavior on a pre-determined set of input sequences. This approach,
however, fails to provide guarantees about the correctness of the
implementation on all possible input sequences. Consequently, when a
system is running, it is hard to guarantee whether the current
execution of the system is correct or not using the two traditional
methods. Therefore, the approach of continuously monitoring a running
system has received much attention, as it attempts to overcome the
difficulties encountered by the two traditional methods for checking
the correctness of the current execution of the system.
We describe a framework that provides assurance on the correctness of
program execution at run-time. This approach is based on the
Monitoring and Checking (MAC) architecture, and complements the two
traditional approaches for ensuring that a system is correct, namely
static analysis and testing. Unlike these approaches which try to
ensure that all possible executions of the system are correct, this
approach ensures only that the current execution of the system is
correct. The MAC architecture consists of three components: filter,
event recognizer, and run-time checker. The filter extracts low-level
information, in the form of values of program variables, from the
instrumented system code, and sends it to the event recognizer. From
this low-level information, the event recognizer detects the
occurrence of abstract events, and informs the run-time checker about
these. The run-time checker then, based on the events, checks the
conformance of the behavior of the system on the current execution, to
the formal requirement specification for the system.
[PCL98b]
Probabilistic Resource Failure in Real-Time Process Algebra
Anna Philippou, Rance Cleaveland, Insup Lee, Scott Smolka, and Oleg Sokolsky
PACSR, a probabilistic extension of the real-time process algebra ACSR, is presented. The extension is built upon a novel treatment of the notion of a resource. In ACSR, resources are used to model contention in accessing physical devices. Here, resources are invested with the ability to fail and are associated with a probability of failure. The resulting formalism allows one to perform probabilistic analysis of real-time system specifications in the presence of resource failures. A probabilistic variant of Hennessy-Milner logic with until is presented. The logic features an until operator which is parameterized by both a probabilistic constraint and a regular expression over observable actions. This style of parameterization allows the application of probabilistic constraints to complex execution fragments. A model-checking algorithm for the proposed logic is also
given. Finally, PACSR and the logic are illustrated with a telecommunications example.
[PSL98a]
Specifying Failures and Recoveries in PACSR
Anna Philippou, Oleg Sokolsky, Insup Lee, Rance Cleaveland, and Scott Smolka
The paper presents PACSR, a probabilistic extension of a real-time process algebra ACSR. The extension is built upon a novel treatment of the notion of a resource. In ACSR, resources are used to model contention in accessing physical devices such as processors, memory modules, and communication links, or any other reusable resource of limited capacity. Here, we invest resources with an ability to fail and associate, with every resource, a probability of its failure. The resulting formalism allows us to perform probabilistic analysis of real-time system specifications in the presence of resource failures. An attractive feature of PACSR is the ability to express failure-recovery actions easily.
We perform probabilistic reachability analysis for PACSR specifications that allows us to compute the probability of occurrence of an undesirable event. We illustrate PACSR specification and analysis by means of a telecommunications example.
[SYL98]
Verification of the Redundancy Management System for Space Launch Vehicle
Oleg Sokolsky, Mohamed Younis, Insup Lee, Hee-Hwan Kwak, and Jeff Zhou
In the recent years, formal methods has been widely recognized as effective techniques to uncover design errors that could be missed by a conventional software engineering process. This paper describes our experience with using formal methods in analyzing the Redundancy Management System (RMS) for a Space Launch Vehicle. RMS is developed by AlliedSignal Inc. for the avionics of NASA's new space shuttle, called VentureStar, that meets the expectations for space missions in the 21st century. A process-algebraic formalism is used to construct a formal specification based on the actual RMS design specifications. Analysis is performed using PARAGON, a toolset for formal specification and verification of distributed real-time systems. A number of real-time and fault-tolerance properties were verified, allowing for some errors in the RMS pseudocode to be detected. The paper discusses the translation of the RMS specification into process algebra formal notation and results of the formal verification.
[KCL98]
Symbolic weak Bisimulation for Value-Passing Calculi
Hee-Hwan Kwak, Jin-Young Choi, Insup Lee and Anna Philippou
Bisimulation equivalence has proved to be a useful notion for providing semantics to process calculi,
and it has been an object of rigorous study within the concurrency theory community. Recently there have
been significant efforts for extending bisimulation techniques to encompass process calculi that allow the
communication of data, that is value-passing calculi. A main challenge in achieving this has been the fact
that in value-passing processes, where the values are from an infinite domain, checking for process equivalence
involves comparing an infinite number of behaviors. Central among work in this area is the approach in which
a new notion of process semantics, namely symbolic semantics, is proposed as a means of expressing a class
of value-passing processes as finite graphs, although their traditional underlying graphs are infinite. This paper
presents new algorithms for computing symbolic weak bisimulation for value-passing processes. These algorithms
are built on the basis of a new formulation of late weak bisimulation which we propose. Unlike the traditional
definition, this formulation allows the use of a single symbolic weak transition relation for expressing both
early and late bisimulations.
In addition to being easy to implement, our algorithms highlight the distinction between early and late weak
bisimulations. Furthermore, we propose a simple variation of symbolic transition graphs with assignment
proposed by Lin, in which the order of assignments and actions in transitions is exchanged. We believe that
the resulting graphs are easier to construct and more intuitive to understand.
[BrLe97]
A Process Algebra of Communicating Shared Resources
with Dense Time and Priorities
Patrice Bremond-Gregoire, Insup Lee
The correctness of real-time distributed systems depends not only on
the function they compute but also on their timing characteristics.
Furthermore, those characteristics are strongly influenced by the
delays due to synchronization and resource availability. Process
algebras have been used successfully to define and prove correctness
of distributed systems. More recently, there has been a lot of
activity to extend their application to real-time systems. The
problem with most current approaches is that they ignore resource
constraints and assume either maximum parallelism (i.e., unlimited
resources) or pure interleaving (i.e., single resource). Algebra of
Communicating Shared Resources (ACSR) is a process algebra designed
for the formal specification and manipulation of distributed systems
with resources and real-time constraints. A dense time domain
provides a more natural way of specifying systems compared to the
usual discrete time. Priorities provide a measure of urgency for
each action and can be used to ensure that deadlines are met.
In ACSR, processes are specified using resource bound, timed actions
and instantaneous synchronization events. Processes can be combined
using traditional operators such as nondeterministic choice and
parallel execution. Specialized operators allow the specification of
real-time behavior and constraints. The semantics of ACSR is defined
as a labeled transition system. Equivalence between processes is
based on the notion of strong bisimulation. A sound and complete set
of algebraic laws can be used to transform almost any ACSR process
into a normal form.
[BCL97b]
A Complete Axiomatization of Finite-state (ACSR) Processes
Patrice Bremond-Gregoire, Jin-Young Choi and Insup Lee
A real-time process algebra, called ACSR, has been developed to
facilitate the specification and analysis of real-time systems. ACSR
supports synchronous timed actions and asynchronous instantaneous
events. Timed actions are used to represent the usage of resources
and to model the passage of time. Events are used to capture
synchronization between processes. To be able to specify real-time
systems accurately, ACSR supports a notion of priority that can be
used to arbitrate among timed actions competing for the use of
resources and among events that are ready for synchronization. In
addition to operators common to process algebra, ACSR includes the
scope operator which can be used to model timeouts and interrupts.
Equivalence between ACSR terms is based on the notion of strong
bisimulation. This paper briefly describes the syntax and semantics
of ACSR and then presents a set of algebraic laws that can be used to
prove equivalence of ACSR processes. The contribution of this paper
is the soundness and completeness proofs of this set of laws. The
completeness proof is for finite-state ACSR processes, which are
defined to be processes without free variables under parallel operator
or scope operator.
[LeSo97]
A Graphical Property Specification Language
Insup Lee and Oleg Sokolsky
The paper presents a language for specification of high-level properties of real-time systems. The language is based on a temporal logic. Properties expressed as temporal logic formulas are known to be very obscure. In the design of the language, we tried to identify sources of this and make expressions as easy to comprehend as possible. To enhance flexibility of the language, we employ a two-level approach: expert level and user level. This allows to hide obscure formal notation from the user, and at the same time adjust the language to any desired problem domain. User-level expressions have
graphical notation, which brings out the structure of expressions in a natural way and leads to easier understanding of formulas.
[BLS97]
Operational Semantics for Visual Simulation in PARAGON
Hanêne Ben-Abdallah, Insup Lee, and Oleg Sokolsky
In the case of safety-critical systems simulation is more credible when it is derived through a mathematically sound interpretation of a specification. In this paper, we describe the foundation and tool to support visual simulation of specifications within PARAGON, a toolset for the formal specification, analysis and testing of real-time, resource-bound systems.
Visual simulation executes a real-time system specification that is described in the Graphical Communicating Shared Resources language (GCSR). It is based on the operational semantics of GCSR which describes all possible execution steps of a GCSR specification in terms of the GCSR graphical entities.
The rules of the operational semantics for GCSR have been implemented as a simulator within PARAGON. The GCSR simulator provides a visual animation of a GCSR model, which makes it easier to understand directly the behavior of a model as oppose to examining its execution traces.
[ClLe97b]
Automatic Test Generation for the Analysis of a Real-Time System: Case Study
Duncan Clarke and Insup Lee
We present a framework for testing timing constraints of real-time
systems. Our tests are automatically derived from specifications of
minimum and maximum allowable delays between input/output events in
the execution of a system. Our test derivation scheme uses a
graphical specification formalism for timing constraints, and the
real-time process algebra Algebra of Communicating Shared Resources
(ACSR) for representing tests and process models. The use of ACSR to
describe test sequences has two main advantages. First, tests can be
applied to an ACSR model of the software system within the ACSR
semantic framework for model validation purposes. Second, ACSR has
concise notation and a precise semantics that will facilitate the
translation of real-time tests into a software test language for
software validation purposes. The major benefit of our approach is
that it can be used to validate a design specification which has too
many states for exhaustive state space exploration based analysis. As
an illustration of this benefit, we describe the case study of using the
automatic derivation of tests from timing specifications for the
analysis of the Philips Audio Control Protocol.
[ClLe97a]
Automatic Generation of Tests for Timing Constraints from
Requirements
Duncan Clarke and Insup Lee
We present a framework for testing timing constraints of real-time
systems. Our tests are automatically derived from specifications of
minimum and maximum allowable delays between input/output events in
the execution of a system. Our test derivation scheme uses a
graphical specification formalism for timing constraints, and the
real-time process algebra Algebra of Communicating Shared
Resources (ACSR) for representing tests and process models. The use
of ACSR to describe test sequences has two main advantages. First,
tests can be applied to an ACSR model of the software system
within the ACSR semantic framework for model validation purposes.
Second, ACSR has concise notation and a precise semantics that will
facilitate the translation of real-time tests into a software test
language for software validation purposes.
[BCL97a]
PARAGON: A Paradigm for the Specification, Verification,
and Testing of Real-Time Systems
Hanêne Ben-Abdallah, Duncan Clarke, Insup Lee, and Oleg Sokolsky
The PARAGON toolset provides an environment for the modular and
hierarchical design of resource-bound, real-time systems. It offers
well-integrated graphical and textual specification languages with
formal semantics. Both languages are based on the Algebra of
Communicating Shared Resources (ACSR), a process algebra with explicit
notions of time, resources and priority. The integration of the three
notions widens the applicability of the PARAGON formalisms to embedded
systems, control systems, and fault-tolerant systems where run-time
resource requirements must be considered during the design phase. To
facilitate the design of complex systems, PARAGON allows a designer to
describe a system incrementally through refinement steps that preserve
system properties. To increase dependentability of system models,
PARAGON offers three types of analysis: automated verification of
system requirements, interactive simulation, and testing. In this
paper, we demonstrate the design methodology that
PARAGON offers through examples.
[BLK97]
The Integrated Specification and Analysis of Functional, Temporal,
and Resource Requirements
Hanêne Ben-Abdallah, Insup Lee and Young Si Kim
The Graphical Communicating Shared Resources, GCSR, is a
specification language with a precise, operational semantics for
the specification and analysis of real-time systems. GCSR allows
a designer to integrate the functional and temporal requirements
of a real-time system along with its run-time resource
requirements. The integration is orthogonal in the sense that it
produces system models that are easy to modify, e.g., to reflect
different resource requirements, allocations and scheduling
disciplines. In addition, it renders the verification of resource
related requirements natural and straightforward. The formal
semantics of GCSR allows the simulation of a system model and the
thorough verification of system requirements through equivalence
checking and state space exploration. This paper reviews GCSR and
reports our experience with the production cell case study.
[Ben96]
GCSR: A Graphical Language for the Specification, Refinementt, and Analysis of Real-Time Systems
Hanêne Ben-Abdallah
The Communicating Shared Resources (CSR) paradigm is an ongoing
project at the University of Pennsylvania to build a
framework for the development of real-time systems.
This project has been motivated by a demand for a
rigorous framework in which various design alternatives for a
real-time system can be formally specified and
rigorously analyzed and tested before implementation. This is an
effort to reduce the potentially high cost associated with incorrect
operation of real-time systems which are often embedded in
safety-critical applications.
The work presented in this thesis is a first step towards
incorporating software engineering practices into the CSR paradigm.
This is achieved, on one hand, by developing a formal, graphical CSR
formalism, the Graphical Communicating Shared Resources (GCSR); the
GCSR language adopts the intuitive concepts of nodes and edges in state
diagrams, an informal specification language that is popular within
the software engineering community.
In addition, defining a refinement theory for GCSR allows the
development of real-time systems within this formalism in a top-down
and modular fashion, also a popular design methodology within the
software engineering community.
The GCSR language adopts a syntax that allows a modular and
hierarchical, thus, scalable description of a real-time system. It
supports notions of communication through events, interrupt,
concurrency, and time to describe the functional and temporal
requirements of a real-time system. In addition, GCSR allows the
explicit representation of resources and priorities to resolve
resource contention, in such a way that produces easy to understand
and modify specifications. The semantics of GCSR is defined
operationally either through a direct translation of a GCSR
description to a labeled transition system, or indirectly through a
sound translation to the Algebra of Communicating Shared Resources
(ACSR) [LBG94], a timed process algebra that also has an
operational semantics. The GCSR-ACSR correspondence makes GCSR
benefit from process algebraic analysis techniques such as equivalence
checking, state space exploration, testing as well as simulation. In
addition, the tight correspondence between GCSR and ACSR makes it
possible to use the graphical and textual notations interchangeably
and to have a sound theory for graphical transformation operations,
e.g., to minimize the number of edges and nodes in a GCSR
specification without affecting the behavioral description.
To support the top-down and modular development of a real-time
specification in GCSR, we have augmented ACSR and thus GCSR with a
refinement theory. The refinement theory allows relabeling of events,
addition of implementation events, and substitution of a time and
resource-consuming action with a process that may use fewer or more
resources than the refined action. Consistency between an abstract
specification and a refined specification is defined in terms of an
ordering relation over traces that is extended to sets of traces
according to the Hoare ordering or Egli-Milner ordering. The trace
ordering relation relates traces that share timing properties such as
equal duration and preservation of timed occurrences of communication
events of the abstract specification. To facilitate the practical use
of the refinement theory, we have characterized the extended trace
ordering relations by a set of transformation rules that syntactically
derive a refined process from an abstract one. The transformation
rules define basic graphical operations that represent GCSR
refinements.
To experiment with the GCSR language and its refinement theory, we
have developed a tool set that allows the specification, refinement,
and analysis of real-time systems modeled in GCSR. We report our
evaluation in the case of the Production Cell case
study.
[BBL96]
Ordering Processes in a Real-Time Process Algebra
Patrice Bremond-Gregoire, Hanêne Ben-Abdallah and Insup Lee
The Algebra of Communicating Shared Resources (ACSR) is a timed
process algebra for the formal specification and analysis of
distributed, real-time systems. It features a dense time domain,
resources, and priorities. Our goal is to make ACSR suitable for the
stepwise, modular design of real-time systems, where several
specifications can be constructed with various degree of
desirability. Some may use more resources; some may be faster. In
this paper, we explore several ordering relations over ACSR processes.
Our method defines an ordering relation over execution traces, and
then extends the trace relation to order sets of traces, a possible
semantics of ACSR processes.
[BKL96]
Schedulability and Safety Analysis in the Graphical Communicating
Shared Resources
Hanêne Ben-Abdallah, Young Si Kim and Insup Lee
Graphical Communicating Shared Resources is a formal language for the
specification and analysis of real-time systems, including
their functional, temporal and resource requirements. GCSR
supports the explicit representation of system resources and
priorities to arbitrate resource contentions. These features allow
a designer to examine resource inherent constraints and to
experiment with various resource allocations and scheduling
disciplines in order to produce a more dependable specification.
In addition, GCSR has a precise operational semantics and notions
of equivalence that allow the execution and formal analysis of a
specification. In this paper, we show how to model a scheduling
discipline and verify schedulability and safety properties within
GCSR. We illustrate our method through a mobile robotic
application.
[LBC96]
A Process Algebraic Method for the Specification
and Analysis of Real-Time Systems
Insup Lee, Hanêne Ben-Abdallah, Jin-Young Choi
This chapter describes a timed process algebra, called ACSR, which
supports time-consuming actions and instantaneous events. Actions
model the usage of shared resources and the passage of time, whereas
events allow synchronization between processes. To be able to specify
real-time systems accurately, ACSR supports static priorities that can
be used to arbitrate between actions competing for shared resources
and between events that are ready for synchronization. ACSR also
offers different notions of equivalence that can be used to verify
that two processes behave the same. ACSR is illustrated through the
specification and analysis of a scheduler example, as well as three
variants of the railroad crossing problem.
[ClLe96]
A Hybrid Approach to Formal Verification
Applied to an ATM Switching System
Duncan Clarke and Insup Lee
Verifying the correctness of real-time system models by traditional
approaches that depend on the exploration of the entire system state
space is impractical for large systems. In contrast, testing allows
the search for violations of a property to be narrowed to a relatively
small portion of the overall state space based on assumptions
regarding the structure of an implementation. We present a hybrid
approach that exploits formal methods to verify subcomponents of a
system and testing to gain confidence in the correctness of the
assembled system. The feasibility of the approach is demonstrated by
application of the method to a process algebra model of the Sunshine
ATM switching network.
[KaLe96]
An Efficient State Space Generation for the Analysis of Real-time Systems
Inhye Kang, Insup Lee
State explosion is a well-known problem that impedes analysis and
testing based on state-space exploration. This problem is particularly
serious in real-time systems because unbounded time values cause
the state space to be infinite over for simple systems. In this paper,
we present an algorithm that produces a compact representation of
the reachable state space of a real-time system.
The algorithm yields a small state space, but still retains enough timing information for analysis. To avoid the state explosion which can be caused by simply adding time values to states, our algorithm first
uses history equivalence and transition bisimulation to collapse states
into equivalent classes. In this approach, equivalent states have
identical observable events although transitions into the states may
happen at different times. The algorithm then
augments the resultant state space with timing relations that
describe time distances between transition executions. For example, the
relation @(tr1)+3 <= @(tr2) <= @(tr1)+5 means that transition
tr1 is taken 3 to 5 time units before transition tr2 is taken. This
is used to analyze timing properties such as minimum and maximum time
distances between events. To show the effectiveness of our algorithm,
we have implemented the algorithm and have analyzed several example
applications.
[CLX95a]
VERSA: A Tool for the Specification and Analysis of
Resource-Bound Real-Time Systems
Duncan Clarke, Insup Lee and Hong-Liang Xie
VERSA is a tool that assists in the algebraic analysis of real-time
systems. It is based on ACSR, a timed process algebra designed to
express resource-bound real-time distributed systems. VERSA supports
the analysis of real-time processes through algebraic rewriting,
interactive execution, and equivalence testing. This paper begins by
presenting a brief overview of the process algebra ACSR, its syntax,
operational semantics, and equivalence relations. VERSA's process and
command syntax, its algebraic rewrite system, and its state-based
analysis features are described fully. The presentation includes
examples that illustrate the salient features of ACSR, and output from
sample VERSA sessions that demonstrate the application of the tool to
real-time systems analysis.
[BLC95]
A Graphical Language with Formal Semantics for the
Specification and Analysis of Real-Time Systems
Hanêne Ben-Abdallah, Insup Lee, and Jin-Young Choi
Graphical Communicating Shared Resources, GCSR, is a formal language
for the specification and analysis of real-time systems including
their functional and resource requirements. GCSR allows a modular and
hierarchical, and thus, scalable specification of a real-time system.
GCSR supports notions of communication through events, interrupt,
concurrency, and time to describe a real-time system. In addition,
GCSR allows the explicit representation of resources and priorities to
arbitrate resource contention in a natural way that produces easy to
understand and modify specifications. The semantics of GCSR is the
Algebra of Communicating Shared Resources, a timed process algebra
with operational semantics. In addition to precise semantics and
executability, The process algebra provides behavioral equivalence
relations which can be used to verify the correctness of one GCSR
specification with respect to the other.
[CLX95b]
The Specification and Schedulability Analysis of
Real-Time Systems using ACSR
Jin-Young Choi, Insup Lee and Hong-Liang Xie
To engineer reliable real-time systems, it is desirable to detect
timing anomalies early in the development process. However, there
is little work addressing the problem of accurately predicting
timing properties of real-time systems before implementations are
developed. This paper describes an approach to the specification
and schedulability analysis of real-time systems based on the timed
process algebra ACSR-VP, which is an extension of ACSR with value-passing
communication and dynamic priorities. Combined with the existing features
of ACSR for representing time, synchronization and resource requirements,
ACSR-VP is capable of specifying a variety of real-time systems with
different scheduling disciplines in a modular fashion. Moreover, we
can perform schedulability analysis on real-time systems specified in
ACSR-VP automatically by checking for a certain bisimulation relation.
[ClLe95]
Testing Real-Time Constraints in a Process Algebraic Setting
Duncan Clarke and Insup Lee
Verifying timing properties of real-time systems by traditional
approaches that depend on the exploration of the entire system state
space is impractical for large systems. In contrast, testing allows
the search for violations of a property to be narrowed to a relatively
small portion of the overall state space, based on assumptions
regarding the structure of an implementation. We present a domain
testing based technique for verifying timing constraints of real-time
systems, given timing constraints specified as minimum and maximum
allowable delays between input/output events. The testing methodology
is presented in a process algebraic setting where it is an efficient
alternative to model checking for verifying system timing properties.
An example illustrates the application of our testing technique to a
timed interactive system.
[CLK94]
Timing Analysis of Superscalar Processor Programs Using ACSR
Jin-Young Choi, Insup Lee, and Inhye Kang
This paper illustrates a formal technique for describing the timing
properties and resource constraints of pipelined superscalar processor
instructions at high level. Superscalar processors can issue and
execute multiple instructions simultaneously. The degree of
parallelism depends on the multiplicity of hardware functional units
as well as data dependencies among instructions. Thus, the timing
properties of a superscalar program is difficult to analyze and
predict.
We describe how to model the instruction-level architecture of a
superscalar processor using ACSR and how to derive the temporal
behavior of an assembly program using the ACSR laws. The salient
aspect of ACSR is that the notions of time, resources and priorities
are supported directly in the algebra. Our approach is to model
superscalar processor registers as ACSR resources, instructions as
ACSR processes, and use ACSR priorities to achieve maximum possible
instruction-level parallelism.
[ChKa94]
Translation of Modechart Specification to
Algebra of Communicating Shared Resources
Jin-Young Choi and Inhye Kang
In this paper, we give a translation from Modechart Specification to
Algebra of Communicating Shared Resources (ACSR). That is, we give a
clear, consistent and precise semantics of Modechart using ACSR. This
makes it possible to combine the advantages of a graphical language
with the rigor of process algebra.
[LBG94]
A Process Algebraic Approach to the Specification and Analysis of
Resource-Bound Real-Time Systems
Insup Lee, Patrice Bremond-Gregoire, and Richard Gerber
Recently, significant progress has been made in the development of
timed process algebras for the specification and analysis of real-time
systems. This paper describes a timed process algebra called ACSR.
ACSR supports synchronous timed actions and asynchronous instantaneous
events. Timed actions are used to represent the usage of resources
and to model the passage of time. Events are used to capture
synchronization between processes. To be able to specify real systems
accurately, ACSR supports a notion of priority that can be used to
arbitrate among timed actions competing for the use of resources and
among events that are ready for synchronization. The paper also
includes a brief overview of other timed process algebras and
discusses similarities and differences between them and ACSR.
[Cla94]
VERSA: Verification, Execution and Rewrite System for ACSR
Duncan Clarke
VERSA is a tool for the automated analysis of resource-bound real-time
systems using the Algebra of Communicating Shared Resources (ACSR).
This document serves as an introduction to the tool for beginning
users, and as a reference for process and command syntax for users of
all experience levels. Coverage includes a complete description of
process and command syntax, examples of usage, and tables of operators,
built-in functions and algebraic laws. Two detailed examples
demonstrate the application of VERSA to canonical examples from the
literature.
This version of the VERSA user's guide reflects the 95.09.10 version
of the tool. The latest version of VERSA is available by anonymous
ftp from ftp.cis.upenn.edu in directory pub/rtg, and through the
World-Wide Web via the Penn Real-Time Group home page http://rtg.cis.upenn.edu/.
[KaLe94]
State Minimization for Concurrent System Analysis
Based on State Space Exploration
Inhye Kang and Insup Lee
A fundamental issue in the automated analysis of concurrent systems is
the efficient generation of the reachable state space. Since it is
not possible to explore all the reachable states of a system if the
number of states is very large or infinite, we need to develop
techniques for minimizing the state space. This paper presents our
approach to cluster subsets of states into equivalent classes. We
assume that concurrent systems are specified as communicating state
machines with arbitrary data space. We describe a procedure for
constructing a minimal reachability state graph from communicating
state machines. As an illustration of our approach, we analyze a
producer-consumer program written in Ada.
[DLW91]
Timed Atomic Commitment
Susan B. Davidson, Insup Lee, Victor Wolfe
In a large class of hard-real-time control applications,
components execute concurrently on distributed nodes
and must coordinate, under timing constraints, to perform the
control task. As such, they perform a type of atomic commitment.
Traditional atomic commitment differs, however, because there
are no timing constraints; agreement is eventual. We therefore
define timed atomic commitment (TAC) which requires the processes
to be functionally consistent, but allows the outcome to
include an exceptional state, indicating that timing constraints
have been violated. We then present centralized and decentralized
protocols to implement TAC and a high-level language construct
that facilitates its use in distributed real-time programming.
[WDL93]
RTC: Language Support for Real-Time Concurrency
Victor Wolfe, Susan Davidson and Insup Lee
This paper presents a model and language constructs for expressing timing and
concurrency requirements in distributed real-time programs. Our approach
combines an abstract data type paradigm for the specification of shared
resources and a distributed transaction-based paradigm for the specification
of application processes. Resources provide abstract views of shared system
entities, such as devices and data structures. Each resource has a state and
defines a set of actions that can be invoked by processes to examine or
change its state. A resource also specifies scheduling constraints on the
execution of its actions to ensure its consistency. Processes access resources
by invoking actions and by expressing precedence, execution and timing
constraits on action invocations. The implementation of our language constructs
and the use of this system to control the simulation of a distributed
robotics application is also described.
[WDL91]
RTC: Language Support for Real-Time Concurrency
Victor Wolfe, Susan Davidson and Insup Lee
This paper presents language constructs for the expression of timing and
concurrency requirements in distributed real-time programs. The programming
paradigm combines an object-based paradigm for the specification of shared
resources, a distributed transaction-based paradigm for the specification of
application processes, and explicit timing constraint expression. An
implementation of the language constructs with real-time scheduling and
locking for concurrency control is also described.
[LeDa90]
A Performance Analysis of Timed Synchronous Comunication Primitives
Insup Lee, Susan B. Davidson
Two algorithms for timed synchronous communication between a single sender and single receiver have recently appeared in the literature. Each weakens the definition of -Y´correct¡ timed synchronous communication in a different way, and exhibits a different ´undesirable¡ behavior. In this paper, their performance is analyzed, and their sensitivity to various parameters is discussed. These parameters include how long the processes are willing to wait for communication to be successful, how well synchronized the processes are, the assumed upper bound on message delay, and the actual end-to-end message delay distribution. We conclude by discussing the fault tolerance of the algorithms, and propose a mixed strategy that avoids some of the performance problems.
[LDW87]
Motivating Time As A First Class Entity
Insup Lee, Susan Davidson, and Victor Wolfe
In hard real-time applications, programs must not only be functionally correct but must also meet timing constraints. Unfortunately, little work has been done to allow a high-level incorporation of timing constraints into distributed real-time programs. Instead the programmer is required to ensure system timing through a complicated synchronization process or through low-level programming, making it difficult to create and modify programs. In this report, we describe six features that must be integrated into a high level language and underlying support system in order to promote time to a first class position in distributed real-time programming systems: expressibility of time, real-time communication, enforcement of timing constraints, fault tolerance to violations of constraints, ensuring distributed system state consistency in the time domain, and static timing verification. For each feature we describe what is required, what related work had been performed, and why this work does not adequately provide sufficient capabilities for distributed real-time programming. We then briefly outline an integrated approach to provide these six features using a high-level distributed programming language and system tools such as compilers, operating systems, and timing analyzers to enforce and verify timing constraints.
[LeDa87]
Adding Time to Synchronous Process Communications
Insup Lee, Susan B. Davidson
In distributed real-time systems, communicating processes cannot be delayed for arbitrary amounts of time while waiting for messages. Thus, communication primitives used for real-time programming usually allow the inclusion of a deadline or timeout to limit potential delays due to synchronization. This paper interprets timed synchronous communication as having absolute deadlines. Various ways of implementing deadlines are discusssed, and two useful timed synchronous communication problems are identified which differ in the number of of participating senders and receivers and type of synchronous communication. For each problem, a simple algorithm is presented and shown to be correct. The algorithms are shown to guarantee maximal success and to require the smallest delay intervals during which processes wait for synchronous communication. We also evaluate the number of messages used to reach agreement.
[LeGe85]
Language Constructs for Distributed Real-Time Programming
Insup Lee and Vijay Gehlot
For many distributed applications, it is not sufficient for programs to be logically correct. In addition, they must satisfy various timing constraints. This paper discusses primitives that support the construction of distributed real-time programs. Our discussion is focused in two areas: timing specification and communication. To allow the specifications of timing constraints, we introduce the language constructs for defining temporal scope and specifying message deadline. We also identify communication primitives needed for real-time programming. The issues underlying the selection of the primitives are explained, including handling of timing exceptions. The primitives will eventually be provided as part of a distributed programming system that will be used to construct distributed multi-sensory systems.
|
