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

[EES06]
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 Rigorous 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 Сha, 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.

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

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

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

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

[PSL98]
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 21^st 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.

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.