Reasoning about real-time repetitions: terminating and nonterminating

It is common for a real-time system to contain a nonterminating process monitoring an input and controlling an output. Hence, a real-time program development method needs to support nonterminating repetitions. In this paper we develop a general proof rule for reasoning about possibly nonterminating repetitions. The rule makes use of a Floyd-Hoare-style loop invariant that is maintained by each iteration of the repetition, a Jones-style relation between the pre- and post-states on each iteration, and a deadline specifying an upper bound on the starting time of each iteration. The general rule is proved correct with respect to a predicative semantics. In the case of a terminating repetition the rule reduces to the standard rule extended to handle real time. Other special cases include repetitions whose bodies are guaranteed to terminate, nonterminating repetitions with the constant true as a guard, and repetitions whose termination is guaranteed by the inclusion of a fixed deadline. (C) 2002 Elsevier Science B.V. All rights reserved.

Procedures and parameters in the real-time program refinement calculus

The real-time refinement calculus is a formal method for the systematic derivation of real-time programs from real-time specifications in a style similar to the non-real-time refinement calculi of Back and Morgan. In this paper we extend the real-time refinement calculus with procedures and provide refinement rules for refining real-time specifications to procedure calls. A real-time specification can include constraints on, not only what outputs are produced, but also when they are produced. The derived programs can also include time constraints oil when certain points in the program must be reached; these are expressed in the form of deadline commands. Such programs are machine independent. An important consequence of the approach taken is that, not only are the specifications machine independent, but the whole refinement process is machine independent. To implement the machine independent code on a target machine one has a separate task of showing that the compiled machine code will reach all its deadlines before they expire. For real-time programs, externally observable input and output variables are essential. These differ from local variables in that their values are observable over the duration of the execution of the program. Hence procedures require input and output parameter mechanisms that are references to the actual parameters so that changes to external inputs are observable within the procedure and changes to output parameters are externally observable. In addition, we allow value and result parameters. These may be auxiliary parameters, which are used for reasoning about the correctness of real-time programs as well as in the expression of timing deadlines, but do not lead to any code being generated for them by a compiler. (c) 2006 Elsevier B.V. All rights reserved.

Dynamic binary translation using run-time feedbacks

Dynamic binary translation is the process of translating, modifying and rewriting executable (binary) code from one machine to another at run-time. This process of low-level re-engineering consists of a reverse engineering phase followed by a forward engineering phase. UQDBT, the University of Queensland Dynamic Binary Translator, is a machine-adaptable translator. Adaptability is provided through the specification of properties of machines and their instruction sets, allowing the support of different pairs of source and target machines. Most binary translators are closely bound to a pair of machines, making analyses and code hard to reuse. Like most virtual machines, UQDBT performs generic optimizations that apply to a variety of machines. Frequently executed code is translated to native code by the use of edge weight instrumentation, which makes UQDBT converge more quickly than systems based on instruction speculation. In this paper, we describe the architecture and run-time feedback optimizations performed by the UQDBT system, and provide results obtained in the x86 and SPARC® platforms.

A state-of-practice questionnaire on verification and validation for concurrent programs

Research in verification and validation (V&V) for concurrent programs can be guided by practitioner information. A survey was therefore run to gain state-of-practice information in this context. The survey presented in this paper collected state-of-practice information on V&V technology in concurrency from 35 respondents. The results of the survey can help refine existing V&V technology by providing a better understanding of the context of V&V technology usage. Responses to questions regarding the motivation for selecting V&V technologies can help refine a systematic approach to V&V technology selection.

Maximising the information gained from an experimental analysis of code inspection and static analysis for concurrent Java components

The results of empirical studies are limited to particular contexts, difficult to generalise and the studies themselves are expensive to perform. Despite these problems, empirical studies in software engineering can be made effective and they are important to both researchers and practitioners. The key to their effectiveness lies in the maximisation of the information that can be gained by examining existing studies, conducting power analyses for an accurate minimum sample size and benefiting from previous studies through replication. This approach was applied in a controlled experiment examining the combination of automated static analysis tools and code inspection in the context of verification and validation (V&V) of concurrent Java components. The combination of these V&V technologies was shown to be cost-effective despite the size of the study, which thus contributes to research in V&V technology evaluation.

An efficient algorithm for partitioning parameterized polygons into rectangles

In this paper, we propose an algorithm for partitioning parameterized orthogonal polygons into rectangles. The algorithm is based on the plane-sweep technique and can be used for partitioning polygons which contain holes. The input to the algorithm consists of the contour of a parameterized polygon to be partitioned and the constraints for those parameters which reside in the contour. The algorithm uses horizontal cuts only and generates a minimum number of rectangles whose union is the original orthogonal polygon. The proposed algorithm can be used as the basis to build corner stitching data structure for parameterized VLSI layouts and has been implemented in Java programming language. Copyright © 2010 ACM, Inc.

Spatial indexing for scalability in FCA

The paper provides evidence that spatial indexing structures offer faster resolution of Formal Concept Analysis queries than B-Tree/Hash methods. We show that many Formal Concept Analysis operations, computing the contingent and extent sizes as well as listing the matching objects, enjoy improved performance with the use of spatial indexing structures such as the RD-Tree. Speed improvements can vary up to eighty times faster depending on the data and query. The motivation for our study is the application of Formal Concept Analysis to Semantic File Systems. In such applications millions of formal objects must be dealt with. It has been found that spatial indexing also provides an effective indexing technique for more general purpose applications requiring scalability in Formal Concept Analysis systems. The coverage and benchmarking are presented with general applications in mind.

Assessing Needs for Computer Pest Management Software in Nebraska Agriculture

A mail survey was conducted to assess current computer hardware use and perceived needs of potential users for software related to crop pest management in Nebraska. Surveys were sent to University of Nebraska-Lincoln agricultural extension agents, agribusiness personnel (including independent crop consultants), and crop producers identified by extension agents as computer users. There were no differences between the groups in several aspects of computer hardware use (percentage computer use, percentage IBM-compatible computer, amount of RAM memory, percentage with hard drive, hard drive size, or monitor graphics capability). Responses were similar among the three groups in several areas that are important to crop pest management (pest identification, pest biology, treatment decision making, control options, and pesticide selection), and a majority of each group expressed the need for additional sources of such information about insects, diseases, and weeds. However, agents mentioned vertebrate pest management information as a need more often than the other two groups. Also, majorities of each group expressed an interest in using computer software, if available, to obtain information in these areas. Appropriate software to address these needs should find an audience among all three groups.

Software development for the array computer ILLIAC IV,

"Supported in part by the Advanced Research Projects Agency as administered by the Rome Air Development Center under contract no. US AF 30(602) 4144."

Minimally Invasive Computer-Assisted Stereotactic Fenestration of an Aqueductal Cyst: Case Report

Introduction: Current advances in frame modeling and computer software allow stereotactic procedures to be performed with great accuracy and minimal risk of neural tissue or vascular injury. Case Report: In this report we associate a previously described minimally invasive stereotactic technique with state-of-the-art 3D computer guidance technology to successfully treat a 55-year-old patient with an arachnoidal cyst obstructing the aqueduct of Sylvius. We provide 1 detailed technical information and discuss how this technique deals with previous limitations for stereotactic manipulation of the aqueductal region. We further discuss current advances in neuroendoscopy for treating obstructive hydrocephalus and make comparisons with our proposed technique. Conclusion: We advocate that this technique is not only capable of treating this pathology but it also has the advantages to enable reestablishment of physiological CSF flow thus preventing future brainstem compression by cyst enlargement.

Behavioral Types for Embedded Software - A Survey

At present, there is a variety of formalisms for modeling and analyzing the communication behavior of components. Due to a tremendous increase in size and complexity of embedded systems accompanied by shorter time to market cycles and cost reduction, so called behavioral type systems become more and more important. This chapter presents an overview and a taxonomy of behavioral types. The intentions of this taxonomy are to provide a guidance for software engineers and to form the basis for future research.