Monitoring-Oriented programming (MOP1) [21, 18, 22, 19] is a formal framework for software development and analysis, in which the developer specifies desired properties using definable specification formalisms, along ...
详细信息
Monitoring-Oriented programming (MOP1) [21, 18, 22, 19] is a formal framework for software development and analysis, in which the developer specifies desired properties using definable specification formalisms, along with code to execute when properties are violated or validated. The MOP framework automatically generates monitors from the specified properties and then integrates them together with the user-defined code into the original system. The previous design of MOP only allowed specifications without parameters, so it could not be used to state and monitor safety properties referring to two or more related objects. In this paper we propose a parametric specification-formalism-independent extension of MOP, together with an implementation of JavaMOP that supports parameters. In our current implementation, parametric specifications are translated into AspectJ code and then weaved into the application using off-the-shelf AspectJ compilers;hence, MOP specifications can be seen as formal or logical aspects. Our JavaMOP implementation was extensively evaluated on two benchmarks, Dacapo [14] and Tracematches [8], showing that runtime verification in general and MOP in particular are feasible. In some of the examples, millions of monitor instances are generated, each observing a set of related objects. To keep the runtime overhead of monitoring and event observation low, we devised and implemented a decentralized indexing optimization. Less than 8% of the experiments showed more than 10% runtime overhead;in most cases our tool generates monitoring code as efficient as the hand-optimized code. Despite its genericity, JavaMOP is empirically shown to be more efficient than runtime verification systems specialized and optimized for particular specification formalisms. Many property violations were detected during our experiments;some of them are benign, others indicate defects in programs. Many of these are subtle and hard to find by ordinary testing.
The purpose of this paper is to extend the notions of prime implicates and prime implicants to the basic modal logic κ. We consider a number of different potential definitions of clauses and terms for κ, which we ev...
详细信息
For the typical case in target association, where both the target tracks and the measurements are described with Gaussian random variables, the standard association uses the chi-squared metric, a weighted inner produc...
详细信息
This paper presents a new fuzzy control approach to compressor surge control. A variable area throttle is used in this strategy. The controller uses measurements of flow and the change of flow to determine the control...
详细信息
What we call a "higher-order method" (HOM) is a method that makes mandatory calls to other dynamically-dispatched methods. Examples include template methods as in the Template method design pattern and notif...
详细信息
ISBN:
(纸本)9781595937865
What we call a "higher-order method" (HOM) is a method that makes mandatory calls to other dynamically-dispatched methods. Examples include template methods as in the Template method design pattern and notify methods in the Observer pattern. HOMs are particularly difficult to reason about, because standard pre- and postcondition specifications cannot describe the mandatory calls. For reasoning about such methods, existing approaches use either higher-order logic or traces, but both are complex and verbose. We describe a simple, concise, and modular approach to specifying HOMs We show how to verify calls to HOMs and their code using first-order verification conditions, in a sound and modular way. Verification of client code that calls HOMs can take advantage of the client's knowledge about the mandatory calls to make strong conclusions. Our verification technique validates and explains traditional documentation practice for HOMs, which typically shows their code. However, specifications do not have to expose all of the code to clients, but only enough to determine how the HOM makes its mandatory calls.
A dynamic language promotes ease of use through flexible typing, a focus on high-level programming, and by streamlining the edit-compile-debug cycle. Live languages go beyond dynamic languages with more ease of use fe...
详细信息
ISBN:
(纸本)9781595937865
A dynamic language promotes ease of use through flexible typing, a focus on high-level programming, and by streamlining the edit-compile-debug cycle. Live languages go beyond dynamic languages with more ease of use features. A live language supports live programming that provides programmers with responsive and continuous feedback about how their edits affect program execution. A live language is also based on high-level constructs such as declarative rules so that programmers can write less code. A live language could also provide programmers with responsive semantic feedback to enable time-saving services such as code completion. This paper describes the design of a textual live language that is based on reactive data-flow values known as signals and dynamic inheritance. Our language, Super-Glue, supports live programming with responsive semantic feedback, which we demonstrate with a working prototype.
Our research involves improving performance of programs written in the Java programming language. By selective specialization of generic types, we enable the compiler to eliminate typecasting, and provide type informa...
详细信息
ISBN:
(纸本)9781595938657
Our research involves improving performance of programs written in the Java programming language. By selective specialization of generic types, we enable the compiler to eliminate typecasting, and provide type information to remove dynamic method lookup at runtime. An example of this specialization using Quicksort showed performance improvement of about 25%.
In this 5th international Workshop on SOA and Web Services, we will explore best-practices in the adoption, design, implementation, management and monitoring of SOA- and Web services-related methods, tools and technol...
详细信息
ISBN:
(纸本)9781595938657
In this 5th international Workshop on SOA and Web Services, we will explore best-practices in the adoption, design, implementation, management and monitoring of SOA- and Web services-related methods, tools and technologies. This workshop is a continuation of a highly successful series of workshops at OOPSLA 2006, OOPSLA 2005, OQPSLA 2004, and OQPSLA 2003.
A trace monitor observes an execution trace at runtime;when it recognises a specified sequence of events, the monitor runs extra code. In the aspect-oriented programming community, the idea originated as a generalisat...
详细信息
ISBN:
(纸本)9781595937865
A trace monitor observes an execution trace at runtime;when it recognises a specified sequence of events, the monitor runs extra code. In the aspect-oriented programming community, the idea originated as a generalisation of the advice-trigger mechanism: instead of matching on single events (joinpoints), one matches on a sequence of events. The runtime verification community has been investigating similar mechanisms for a number of years, specifying the event patterns in terms of temporal logic, and applying the monitors to hardware and software. In recent years trace monitors have been adapted for use with mainstream object-oriented languages. In this setting, a crucial feature is to allow the programmer to quantify over groups of related objects when expressing the sequence of events to match. While many language proposals exist for allowing such features, until now no implementation had scalable performance: execution on all but very simple examples was infeasible. This paper rectifies that situation, by identifying two optimisations for generating feasible trace monitors from declarative specifications of the relevant event pattern. We restrict ourselves to optimisations that do not have a significant impact on compile-time: they only analyse the event pattern, and not the monitored code itself. The first optimisation is an important improvement over an earlier proposal in [2] to avoid space leaks. The second optimisation is a form of indexing for partial matches. Such indexing needs to be very carefully designed to avoid introducing new space leaks, and the resulting data structure is highly non-trivial.
When considering the past or the future, dear apprentice, be mindful of the present. If, while considering the past, you become caught in the past, lost in the past, or enslaved by the past, then you have forgotten yo...
详细信息
ISBN:
(纸本)9781595937865
When considering the past or the future, dear apprentice, be mindful of the present. If, while considering the past, you become caught in the past, lost in the past, or enslaved by the past, then you have forgotten yourself in the present. If, while considering the future, you become caught in the future, lost in the future, or enslaved by the future, then you have forgotten yourself in the present. Conversely, when considering the past, if you do not become caught, lost, or enslaved by the past, then you have remained mindful of the present. And if, when considering the future, you do not become caught, lost, or enslaved in the future, then you have remained mindful of the present.
暂无评论