Distributed Real-Time Embedded (DRE) Systems that address safety and mission-critical system requirements are applied in a variety of domains today. Complex, integrated systems like managed satellite clusters expose heterogeneous concerns such as strict timing requirements, complexity in system integration, deployment, and repair; and resilience to faults. Integrating appropriate modeling and analysis techniques into the design of such systems helps ensure predictable, dependable and safe operation upon deployment. This paper describes how we can model and analyze applications for these systems in order to verify system properties such as lack of deadline violations. Our approach is based on (1) formalizing the component operation scheduling using Colored Petri nets (CPN), (2) modeling the abstract temporal behavior of application components, and (3) integrating the business logic and the component operation scheduling models into a concrete CPN, which is then analyzed. This model-driven approach enables a verication-driven workow wherein the application model can be rened and restructured before actual code development.
Safety and mission-critical DRE systems are used in a variety of domains such as avionics, locomotive control, industrial and medical automation. Given the increasing role of software in such systems, growing both in size and complexity, utilizing predictable and dependable software is critical for system safety. To mitigate this complexity, model-driven, component-based software development has become an accepted practice. Applications are built by assembling together small, tested component building blocks that implement a set of services. Models describe what these component blocks are, what interfaces they have, how they are built, how they interact and how they are deployed to realize the domainspecic application.
Complex, managed systems, e.g. a fractionated spacecraft following a mission timeline and hosting distributed software applications expose heterogeneous concerns such as strict timing requirements, complexity in deployment, repair and integration; and resilience to faults. High-security and time-critical software applications hosted on such platforms run concurrently with all of the system-level mission management and failure recovery tasks that are periodically undertaken on the distributed nodes. Once deployed, it is often dicult to obtain low-level access to such remote systems for run-time debugging and evaluation. These types of systems therefore demand advanced design-time modeling and analysis methods to detect possible anomalies in system behavior, such as unacceptable response time, before deployment.
Our team has designed and prototyped a comprehensive information
architecture called Distributed REal-time Managed System (DREMS) [
The principle behind this design-time analysis here is to map the structural
and behavioral specications of the system under analysis into a formal domain
for which analysis tools exist. Using an appropriate model-based abstraction,
the mapping from one domain to another remains valid under successive
renements in system development, including code generation. Application
developers use domain-specic modeling languages to model the component assembly,
component interactions, component execution code, operation sequencing, and
associated temporal properties such as estimated execution times, deadlines etc.
Using such application-specic parameters in the design model, a Colored Petri
net-based (CPN) [
The remainder of this paper is organized as follows. Section 2 presents existing research relating to this paper; Section 3 provides a brief background on the DREMS Infrastructure and on the CPN formalism; Section 4 discusses the problem statement that is evaluated; Section 5 describes how this architecture is abstracted and modeled using CPN; Section 6 investigates the utility and scalability of state space analysis; Section 7 briey describes how the analysis model is generated; Sections 8 and 9 present future extensions to the proposed approach and concluding remarks respectively. 2
In recent years, much of the proliferating work in the development of missioncritical distributed real-time systems addresses the need for Safety and Verication driven Engineering. Structural properties of the system are established using domain-specic modeling tools. Design models are transformed into relevant analysis models to study possible behaviors of the system and identify anomalies. When analyzing timing behavior, typically several exaggerated assumptions such as upper bounds on task execution times, service rates, maximum resource consumption etc are made. The results of system analysis using these assumptions are equally pessimistic. However, real-time systems with high criticality necessitate such assumptions to avoid the consequences of poor design. Predictability of system behavior is achieved by obtaining upper bounds on the system properties.
Petri nets and their extensions have proven to be a powerful formalism for
modeling and analyzing concurrent systems. System designs represented using a
domain-specic modeling languages are often translated into Petri nets for
formal analysis. High-level formalisms such as AADL models have been translated
into Symmetric Nets for qualitative analysis [
In the context of component-based systems, for complete real-time analysis,
signicant information must be obtained about the component assembly, the
interaction patterns and the temporal behavior of components. The real-time
model of the system is composed of real-time models of its constituent parts, each
with its own temporal behavior. Using abstract model descriptors, [
For classes of component-based systems whose component assembly and
application structure change dynamically over time, design-time verication is
observed to be insucient. Incremental re-verication strategies [
DREMS Components: Design and implementation of component-based software applications rests on the principle of assembly: Complex systems are built by composing re-useable interacting components . Components contain functional, business-logic code that implements operations on state variables. Ports facilitate interactions between communicating components. A component-level message queue, with associated infrastructure code, controls the scheduling of operations of the individual components. Figure 1a shows the basic DREMS component.
Each DREMS component supports four basic types of ports for interaction with other collaborating components: Facets, Receptacles, Publishers and Subscribers. A component’s facet is a unique interface that can be invoked either (a) DREMS Component
(b) Component Operation Scheduling
synchronously via remote method invocation (RMI) or asynchronously via
asynchronous method invocation (AMI). A component’s receptacle species an
interface required by the component in order to function correctly. Using its
receptacle, a component can invoke operations on other components using either RMI
or AMI. A publisher port is a single point of data emission and a subscriber
port is a single point of data consumption. Communication between publishers
and subscribers is contingent on the compatibility of their associated topics (i.e.
data types). More details on this component model can be found in [
The DREMS OS scheduler enforces an ARINC-653 [
With Colored Petri nets (CPN) [
Consider a set of mixed-criticality component-based applications that are distributed and deployed across a cluster of embedded computing nodes. Each component has a set of interfaces that it exposes to other components and to the underlying framework. Once deployed, each component works by executing operations placed on its component message queue. Each component is associated with a single executor thread that handles these operation requests. These executor threads are scheduled in conjunction with a known set of highly critical system threads and low priority best-eort threads. Furthermore, the application threads are also subject to a temporally partitioned scheduling scheme. System assumptions include (1) knowledge of the sequence of computational steps of known duration that are executed inside each component operation, (2) knowledge of the worst-case estimated time taken by each computational step, and (3) the estimated worst-case time taken to initiate a remote function call and to process the response, accounting for network-level delays. Using this knowledge about the system, the problem here is to ensure that the temporal behavior of all the application components lies within the bounds laid out by the system specications. Ideally, this is achieved by verifying such system properties as lack of deadline violations for component operations. For scenarios where the system design isn’t complete, e.g. application thread priorities are unknown, the paper describes the utility of an approach to identifying the subset of system behaviors that satisfy timing requirements and provide useful information to designers, e.g. partial thread execution orders. 5
This section briey describes how CPN can be used to build an extensible,
scalable analysis model for component-based software applications. To edit, simulate
and analyze this model, we use the CPN Tools [
The CPN model captures the behavioral semantics of our component model
described in [
Figure 2 shows a top-level structure of the CPN-based analysis model. The place Component Threads holds a token with a list of all executor threads responsible for component interactions. This list is maintained based on thread priorities on each node so that the highest priority ready thread is always chosen rst by the OS scheduler. Timers maintains a list of all infrastructural timers in the application. All timer expiries at a specic clock value 1 are handled by the transition Timer Expiry. A timer can be used in our component model to trigger the execution of a component operation. DREMS components are dormant by default. Once initialized, a component executor is not eligible to run until there is an operation added to the component message queue. To start a sequence of component interactions, periodic or sporadic timers can be used to trigger an operation of a component.
If a timer triggers a component execution, this component is identied as a candidate for scheduling by Schedule Thread. This transition always schedules the highest priority thread that is ready to execute in the active partition on each node. If two threads of equal priority are eligible, the scheduler picks one at random and maintains a round-robin scheduling scheme. If the highest priority thread is not already servicing an operation request, the highest priority operation from its message queue is dequeued and scheduled for execution.
The Component Message Queues place is a list that manages the message queues of all components across all nodes. Every time a component thread exe1 The clock values are integers.
(a) Component Assembly (b) Timing Diagram cutes an operation, the completion of this operation could trigger another component into execution. For instance - the completion of an RMI query on a client component triggers a server-side RMI operation that this server will have to execute. Such interactions are derived from the modeling tools and appropriate tokens are generated in place Interactions. When executing component threads, Execute Thread checks to see if the execution has any eect on the running thread or on other threads. Therefore, when the client thread completes an RMI query, this thread is moved to Blocked Threads and a server RMI operation is placed in Waiting to Enqueue . Later, when the server thread is scheduled, the client is unblocked appropriately. 6
Given a CPN model (that was generated from a component architecture and deployment model), a state-space of the system can be constructed using the semantics of CPN. This state space is innite, however, in practice, it is often sucient to consider some nite subset, starting from a initial state up to a few hyperperiods of the partition scheduler. In order to describe the utility of state space analysis, we consider a simple trajectory planning application (TPA). The component assembly for this application is shown in Figure 3a. A Sensor component periodically publishes on a trigger topic, notifying the Trajectory Planner of the existence of new sensor data. Once the notication is received, the Trajectory Planner makes an RMI call to retrieve the data structure of sensor values, using which the satellite trajectory is updated. The sequence of steps in each of these operations is referred to as the business logic of the operation. This business logic is modeled using a textual language in the modeling tools, in which the designer species the macro execution steps in a component operation along with worst-case estimated time taken on each step. Figure 3b shows the expected timing diagram.
The analyzable states of this system are observed in the markings of the various CPN places in the model. Using the built-in state space analysis in CPN Tools a bounded state space of the system is generated. Using both standard and user-dened queries, this state space is searched to check system properties like lack deadline violations and deadlocks, bounds on response times etc. Deadline Violation Detection: Each time a component operation is scheduled, the clock value of the node is recorded as the "start time" of the operation. If this operation is incomplete when the clock reaches the operation’s deadline, a deadline violation is detected. Using the SearchNodes function in CPN Tools, the deadline violations on any component operation can be identied by observing all component operations each time the node-specic clock progresses. In Figure 3b, the DDS_OP on the Trajectory Planner takes 56 ms to complete, measured from when the operation was enqueued and marked as ready. If the deadline of this operation is set to 50 ms, a state space search would reveal a deadline violation when the clock reaches 51 ms.
Worst-case Trigger-to-Response Time Calculation: For a known trigger operation and desired response operation, the worst-case trigger-to-response time can also be calculated from the generated state space. Using the names of the trigger and response operations, a state space node that presents the earliest completion of the trigger operation and the latest completion of the response operation within the set period is identied. In the Trajectory Planning application, considering the TIMER_OP to be the trigger and the trajectory planning DDS_OP to be the response, the worst-case response time is found to be 68 ms (Trigger completes earliest at 8 ms and response completes latest at 76 ms). Partial Thread Execution Order Generation: In development scenarios where an application developer is aware of the operation-specic timing requirements but not thread priorities, the analysis is capable of identifying partial thread execution orders that satisfy the requirements. If all unknown thread priorities are set to a common value, the generated partial state space will then encapsulate the set of non-deterministic thread execution orders that arise from the scheduling. Using timing requirements of the form - Once Operation A on Component A on Node A completes, Operation B on Component B on Node B must complete within 150 ms , a state space node satisfying this requirement can be identied by querying the generated state space. A backtrace from this node enables assigning thread priorities to ensure the satisfaction of the timing requirement.
Scalability Testing: The size of the generated state space is dependent on the amount of concurrency in the behavior. If all the executing threads had unique priorities, the thread execution order is a constant as the scheduling is priority-based. However, for large systems with groups of applications and increased concurrency, an equally large state space is required to observe the tree of possible thread executions and operational behaviors. This analysis model has been identied to scale well for medium-sized applications, tested up to 100 components distributed on up to 5 computing nodes. Table 1 summarizes these results. As mentioned in Section 5, the control ow and timing details of component operations are directly integrated into the design-time modeling framework. Using the formal domain-specic model of the system, the conguration of the partition scheduling and component assembly are derived and translated into meaningful CPN tokens. The business logic of each component operation is expressed using a textual language with one attribute per interaction per instance of each component being deployed. Model interpreters parse through this complete design model, instantiating CPN model templates and combining these instances to generate a single integrated .cpn le to analyze the entire system. 8
In order to generalize this analysis model and provide exibility, one possible extension to this approach is to cater to other commonly used scheduling schemes, such as EDF, for component operation scheduling; and novel interaction patterns (e.g. reliable broadcast). Also, the current analysis approach inherits the benets and the drawbacks of using pessimistic estimates for execution times. Another possible extension to this approach would be to provide a stochastic schedulability analysis allowing for a trade-o between reliability and cost of resources required by the system. 9
Distributed real-time systems operating in dynamic environments, and running mission-critical applications face strict timing requirements to operate safely. This paper presents a Colored Petri Net-based approach to capture the architecture and temporal behavior of such applications for both qualitative and quantitative schedulability analysis. This analysis model includes a compact, scalable representation of high-level design, accounting for the dynamics of realtime thread execution while exploiting knowledge of component execution code. Exhaustive state space search enables verication and validation of useful and necessary system properties, reducing development costs and increasing reliability for such time-critical systems.
The DARPA System F6 Program and the National Science Foundation (CNS1035655) supported this work. Any opinions, ndings, and conclusions or recommendations expressed in this material are those of the authors and do not reect the views of DARPA or NSF.
References