A taxonomy for classifying runtime verification tools

International Journal on Software Tools for Technology Transfer - Over the last 20 years, runtime verification (RV) has grown into a diverse and active field, which has stimulated the development...     

A monitoring approach for runtime service discovery

Effective runtime service discovery requires identification of services based on different service characteristics such as structural, behavioural, quality, and contextual characteristics. However, current service registries guarantee services described in terms of structural and sometimes quality characteristics and, therefore, it is not always possible to assume that services in them will have all the characteristics required for effective service discovery. In this paper, we describe a monitor-based runtime service discovery framework called MoRSeD. The framework supports service discovery in both push and pull modes of query execution. The push mode of query execution is performed in parallel to the execution of a service-based system, in a proactive way. Both types of queries are specified in a query language called SerDiQueL that allows the representation of structural, behavioral, quality, and contextual conditions of services to be identified. The framework uses a monitor component to verify if behavioral and contextual conditions in the queries can be satisfied by services, based on translations of these conditions into properties represented in event calculus, and verification of the satisfiability of these properties against services. The monitor is also used to support identification that services participating in a service-based system are unavailable, and identification of changes in the behavioral and contextual characteristics of the services. A prototype implementation of the framework has been developed. The framework has been evaluated in terms of comparison of its performance when using and when not using the monitor component.     

Provably correct runtime monitoring

Runtime monitoring is an established technique to enforce a wide range of program safety and security properties. We present a formalization of monitoring and monitor inlining, for the Java Virtual Machine. Monitors are security automata given in a special-purpose monitor specification language, ConSpec. The automata operate on finite or infinite strings of calls to a fixed API, allowing local dependencies on parameter values and heap content. We use a two-level class file annotation scheme to characterize two key properties: (i) that the program is correct with respect to the monitor as a constraint on allowed program behavior, and (ii) that the program has a copy of the given monitor embedded into it. As the main application of these results we sketch a simple inlining algorithm and show how the two-level annotations can be completed to produce a fully annotated program which is valid in the standard sense of Floyd/Hoare logic. This establishes the mediation property that inlined programs are guaranteed to adhere to the intended policy. Furthermore, validity can be checked efficiently using a weakest precondition based annotation checker, thus preparing the ground for on-device checking of policy adherence in a proof-carrying code setting.     

Safer asynchronous runtime monitoring using compensations

Asynchronous monitoring relieves the system from additional overheads induced through online runtime monitoring. The price paid with such monitoring approaches is that the system may proceed further despite having reached an anomalous state. Any actions performed by the system after the error occurring are undesirable, since for instance, an unchecked malicious user access may perform unauthorized actions. In this paper we investigate the use of compensations to enable the undoing of such undesired actions, thus enriching asynchronous monitoring with the ability to restore the system to the original state just after the anomaly had occurred. Furthermore, we show how adaptive synchronisation and desynchronisation of the monitor with the system can also be achieved and report on the use of the proposed approach on an industrial case study of a financial transaction handling system.     

Cobol tools: overview and taxonomy

One of the biggest challenges post-Y2K is legacy renewal, yet many developers have no idea of the number of tools available. The four tools highlighted here represent a range of legacy renewal options, from new GUI front ends to creating components. The tool taxonomy list covers more than 100 tools in various categories along with their URLs. The four main tools considered are: Flexus Cobol sp2, Merant Net Express, Netron Hotrod, and Transoft Component Framework; they represent a cross-sampling of the types of tools available for working with Cobol     

Concurrent runtime monitoring of formally specified programs

A methodology for continuously monitoring a program for specification consistency during program execution is described. Prior development of the formal specification and program is assumed. The program is annotated with constructs from a formal specification language, and the formal specification constructs are transformed into checking code, which is then inserted into the underlying program. Calls to this checking code are inserted into underlying program wherever it can potentially become inconsistent with its specification. If an inconsistency does in fact occur, diagnostic information is provided. The implementation of such a system for Anna (annotated Ada) subtype annotations is presented     

A runtime system

The runtime data structures of the Standard ML of New Jersey compiler are simple yet general. As a result, code generators are easy to implement, programs execute quickly, garbage collectors are easy to implement and work efficiently, and a variety of runtime facilities can be provided with ease.Supported in part by NSF Grants DCR-8603453 and CCR-880-6121     

A runtime system

The runtime data structures of the Standard ML of New Jersey compiler are simple yet general. As a result, code generators are easy to implement, programs execute quickly, garbage collectors are easy to implement and work efficiently, and a variety of runtime facilities can be provided with ease.     

Recovery oriented programming: runtime monitoring of safety and liveness

We introduce the recovery-oriented programming paradigm. Programs that are designed according to the recovery-oriented programming paradigm include, as an integral part, the important safety and liveness properties that the program should respect and the recovery actions that should be executed upon a violation of these properties. We design a pre-compiler that compiles the properties and recovery actions into a code snippet for monitoring properties and enforcing recovery actions upon property violation. Assuming the restartability property of a given program and the existence of a self-stabilizing software platform, the compiled program is able to recover from safety and liveness violations. We provide a generic correctness proof scheme for recovery-oriented programs, proving that the code, as transformed by the pre-compiler, converges to a legal execution in a finite number of steps after experiencing an arbitrary failure.     

基于Multi-agent的实时系统运行故障监控研究

软件密集型装备中常常包含着许多担负监测和控制作用的嵌入式实时系统,它们常常属于安全关键或者任务关键系统(safety-critical/mission-critical system)。为了能够有效解决该类系统中的软件故障检测、诊断与修复任务,本文提出了基于Multi-agent的实时系统运行故障监控框架,旨在利用在多agent的协作构建运行故障监控系统来在系统运行当中验证系统是否满足时序逻辑描述的性质规约,并采用具体的算法进行故障定位和修复。     

虚拟运行环境描述管理工具的研究和实现

针对分布式网络环境中虚拟运行环境的描述、部署和管理问题,设计和实现了一个图形化的虚拟运行环境的描述、部署和管理系统,该系统整合虚拟机技术,通过图形化的方式来描述目标虚拟运行环境的网络拓扑,配置和部署环境中的虚拟机,并提供了对其中虚拟机基本的管理和控制功能.具有通用性、高可扩展性和灵活性的特点.可用于网格以及其它分布式系统.     

基于嵌入式可信平台的运行时监控方法

当前可信计算平台缺乏对自身运行时安全属性的监控,对此,提出一种针对嵌入式可信平台的运行时监控方法。通过自动化的代码插入和运行时实时监控,保证可信平台的运行时安全功能符合设计规范,并保证系统性能和运行状态符合特定条件约束,同时对相应的异常进行实时处理。实验结果表明,随着监控节点数的增长,监控的准确性和实时性提高,而监控开销和异常处理开销处于合理范围。     

Developing and evolving a DSL-based approach for runtime monitoring of systems of systems

Complex software-intensive systems are often described as systems of systems (SoS) due to their heterogeneous architectural elements. As SoS behavior is often only understandable during operation, runtime monitoring is needed to detect deviations from requirements. Today, while diverse monitoring approaches exist, most do not provide what is needed to monitor SoS, e.g., support for dynamically defining and deploying diverse checks across multiple systems. In this paper we report on our experiences of developing, applying, and evolving an approach for monitoring an SoS in the domain of industrial automation software, that is based on a domain-specific language (DSL). We first describe our initial approach to dynamically define and check constraints in SoS at runtime and then motivate and describe its evolution based on requirements elicited in an industry collaboration project. We furthermore describe solutions we have developed to support the evolution of our approach, i.e., a code generation approach and a framework to automate testing the DSL after changes. We evaluate the expressiveness and scalability of our new DSL-based approach using an industrial SoS. We also discuss lessons we learned. Our results show that while developing a DSL-based approach is a good solution to support industrial users, one must prepare the approach for evolution, by making it extensible and adaptable to future scenarios. Particularly, support for automated (re-)generation of tools and code after changes and automated testing are essential.     

A brief account of runtime verification

In this paper, a brief account of the field of runtime verification is given. Starting with a definition of runtime verification, a comparison to well-known verification techniques like model checking and testing is provided, and applications in which runtime verification brings out its distinguishing features are pointed out. Moreover, extensions of runtime verification such as monitor-oriented programming, and monitor-based runtime reflection are sketched and their similarities and differences are discussed. Finally, the use of runtime verification for contract enforcement is briefly pointed out.     

A taxonomy of reasoning mechanisms and data synchronization framework for road excavation productivity monitoring

Project management tasks, such as productivity monitoring and cost estimation, require data to be fused from multiple data sources, which are typically spatial and temporal in nature. In order to fuse a pair of spatial and temporal data sources, a number of different types of reasoning mechanisms are needed. This paper presents a taxonomy of spatial and temporal reasoning mechanisms needed to fuse spatial and temporal data sources to support construction productivity monitoring. In addition, the paper also describes two different approaches (i.e., interpolation and nearest neighbor approaches) that can be used to synchronize the temporal and/or spatial data sources. The developed taxonomy has been validated based on representative queries of construction engineers and managers that are identified in previous research studies. The interpolation and nearest neighbor approaches have been validated with real and simulated construction data sources.     

A survey of Cloud monitoring tools: Taxonomy,capabilities and objectives

The efficient management of Cloud infrastructure and deployments is a topic that is currently attracting significant interest. Complex Cloud deployments can result in an intricate layered structure. Understanding the behaviour of these hierarchical systems and how to manage them optimally are challenging tasks that can be facilitated by pervasive monitoring. Monitoring tools and techniques have an important role to play in this area by gathering the information required to make informed decisions. A broad variety of monitoring tools are available, from general-purpose infrastructure monitoring tools that predate Cloud computing, to high-level application monitoring services that are themselves hosted in the Cloud. Surveying the capabilities of monitoring tools can identify the fitness of these tools in serving certain objectives. Monitoring tools are essential components to deal with various objectives of both Cloud providers and consumers in different Cloud operational areas. We have identified the practical capabilities that an ideal monitoring tool should possess to serve the objectives in these operational areas. Based on these identified capabilities, we present a taxonomy and analyse the monitoring tools to determine their strength and weaknesses. In conclusion, we present our reflections on the analysis, discuss challenges and identify future research trends in the area of Cloud monitoring.     

A taxonomy of computer‐based simulations and its mapping to parallel and distributed systems simulation tools

In recent years, extensive research has been conducted in the area of simulation to model large complex systems and understand their behavior, especially in parallel and distributed systems. At the same time, a variety of design principles and approaches for computer‐based simulation have evolved. As a result, an increasing number of simulation tools have been designed and developed. Therefore, the aim of this paper is to develop a comprehensive taxonomy for design of computer‐based simulations, and apply this taxonomy to categorize and analyze various simulation tools for parallel and distributed systems. Copyright © 2004 John Wiley & Sons, Ltd.