#!/usr/local/bin/php RTG Publications Abstracts
RTG Home  |   PRECISE  |   CIS Home  |   Penn Engineering  |   Penn
RTG Publications Abstracts




[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.




RTG Home  |   PRECISE  |   CIS Home  |   Penn Engineering  |   Penn