169,860 research outputs found
Well-measuring programs
No full text© Copyright 2006 IEEEAny program that measures quantities from its physical environment must compute using correct and consistent units of measurement. Such a program is described as well-measuring. In many systems, particularly embedded control software, paying inadequate attention to units of measurement can result in catastrophe. Unfortunately, current programming languages and tools provide little aid to the programmer attempting to establish or verify the well-measuring property. We present a program analysis technique for inferring and checking the units used within a program. The technique combines traditional Hindley-Milner-style type inference with the use of static single assignment (SSA) form to enable analysis of imperative programs.Phil Cook, Colin Fidge, and David Heme
Applying the Cogito Program Development Environment to Real-Time System Design
No full textWe show how a formal program development environment, previously used for sequential, non-real-time applications only, can be exploited for parallel, real-time system design. A pragmatic approach is adopted, making best use of existing technologies, in order to quickly achieve useful results.
But what if I don't want to wait forever?
No full textWe present an abstract model of the leader election protocol used in the IEEE 1394 High Performance Serial Bus standard. The model is expressed in the probabilistic Guarded Command Language. By formal reasoning based on this description, we establish the probability of the root contention part of the protocol successfully terminating in terms of the number of attempts to do so. Some simple calculations then allow us to establish an upper bound on the time taken for those attempts
Electronic Notes in Theoretical Computer Science: Preface
No full textAbstractThis volume contains the proceedings of Computing: The Australasian Theory Symposium (CATS), held at Bond University, Australia on 29-30 January 2001. CATS is the premier theoretical computer science conference in the Australasian region. It is held annually as part of Australasian Computer Science Week (ACSW). CATS 2001 is the seventh in the series.Previous CATS symposia have concentrated on topics such as complexity and computability, logics, and automata and number theory. This year the scope of the conference was broadened to also encompass formal specification and development methods, and verification tools. This change resulted in an increased number of submissions: 21 papers were submitted, of which 14 were accepted.This increase meant a greater burden on the international Programme Committee. Nevertheless, all papers were subjected to at least two, and in many cases three, formal reviews. Thanks are due to all members of the Programme Committee and their additional reviewers. In particular, Emo Welzl, Robert Stärk, Mariangiola Dezani-Ciancaglini and Rod Downey made outstanding contributions to the reviewing process.The CATS 2001 Programme Committee was as follows.
1Mariangiola Dezani-Ciancaglini (Università di Torino, Italy)2Rod Downey (Victoria University of Wellington, New Zealand)3Colin Fidge (The University of Queensland, Australia)4Lance Fortnow (NEC Research Institute, USA)5Joseph Goguen (University of California at San Diego, USA)6Andrew Martin (Oxford University, United Kingdom)7Ian Mason (University of New England, Australia)8János Pach (New York University, USA)9Igor Shparlinski (Macquarie University, Australia)10Mark Utting (University of Waikato, New Zealand)11Emo Welzl (ETH Zurich, Switzerland)In addition, the following individuals reviewed papers for CATS 2001.
1Marco Bernardo2Mario Coppo3Robbie Gates4Rob Goldblatt5Karl Lermer6Catherine McCartin7Brian Nielsen8Mehmet Orgun9Marina Ribaudo10Peter Robinson11Simona Ronchi della Rocca12Ivano Salvo13Robert Stärk14Frank Stephan15Ewan Tempero16Dominic VerityCATS 2001 is also honoured to host two exceptional invited speakers.
•Prof. Mathai Joseph has a distinguished academic research record which includes significant contributions to multi-task scheduling theory and formal methods for fault-tolerant and real-time systems. Most recently, he has successfully made the challenging transition from academia to industry.•Prof. Carroll Morgan is widely known in the formal methods community for his fundamental contributions to the refinement calculus for deriving computer programs from their specifications. His many publications in the area have helped to popularise the calculus, especially his much cited textbook, Programming from Specifications.David Wolfram, Programme Chair for CATS 2000, provided considerable practical advice on organising the conference. Mike Mislove, Managing Editor of Electronic Notes in Theoretical Computer Science, once again supported publication of the CATS proceedings in that series and helped prepare this volume. Other ACSW 2001 organisers, especially Michael Oudshoorn, Gopal Gupta, Naomi Robinson, Jeanette Niehus and Marcus Randall assisted with practical problems. As part of ACSW, the CATS conference is sponsored by the Computer Science Association whom we thank for their continuing support.Colin Fidge, Guest EditorSoftware Verification Research CentreThe University of QueenslandAustrali
A Set-Theoretic Model for Real-Time Specification and Reasoning
No full textAbstract. Timed-trace formalisms have emerged as a powerful method for specifying and reasoning about concurrent real-time systems. We present a simple variant which builds methodically on set theory, and is thus suitable for use by programmers with little formal methods experience.
Going Beyond Counting First Authors in Author Co-citation Analysis
No full textThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
Mitomycin C in highly myopic eyes - Author reply
No full textOphthalmology. 2005 Feb;112(2):208-18; discussion 219.
Mitomycin C modulation of corneal wound healing after photorefractive keratectomy in highly myopic eyes.
Gambato C, Ghirlando A, Moretto E, Busato F, Midena E.
SourceRefractive Surgery Service and Antimetabolite Therapy Research Unit, Department of Ophthalmology, University of Padova, Padova, Italy.
Abstract
PURPOSE: To evaluate the role of topical mitomycin C in corneal wound healing (CWH) after photorefractive keratectomy (PRK) in highly myopic eyes.
DESIGN: Prospective, double-masked, randomized clinical trial.
PARTICIPANTS: Seventy-two eyes of 36 patients affected by high (>7 diopters) myopia.
METHODS: In each patient, one eye was randomly assigned to PRK with intraoperative topical 0.02% mitomycin C application, and the fellow eye was treated with a placebo. Postoperatively, mitomycin C-treated eyes received artificial tears (3 times daily, tapered in 3 months), whereas the fellow eye was treated with fluorometholone sodium 2% and artificial tears (3 times daily, tapered in 3 months).
MAIN OUTCOME MEASURES: Uncorrected visual acuity (UCVA) and best-corrected visual acuity (BCVA), contrast sensitivity, manifest refraction, and biomicroscopy. Contrast sensitivity was determined using the Pelli-Robson chart. Corneal confocal microscopy documented CWH.
RESULTS: Mean follow-up was 18 months (range, 12-36). No side effects or toxic effects were documented. At 12-month follow-up examination, UCVAs (logarithm of the minimum angle of resolution) were 0.4+/-0.48 and 0.5+/-0.53 (P = .03) in mitomycin C-treated eyes and corticosteroid-treated eyes, respectively. At 1 year, corneal haze developed in 20% of corticosteroid-treated eyes, versus 0% of mitomycin C-treated eyes. At 12, 24, and 36 months, corneal confocal microscopy showed activated keratocytes and extracellular matrix significantly more evident in untreated eyes (Ps = 0.004, 0.024, and 0.046, respectively).
CONCLUSION: Topical intraoperative application of 0.02% mitomycin C can reduce haze formation in highly myopic eyes undergoing PRK.
Comment in
Ophthalmology. 2006 Feb;113(2):357; author reply 357-8
Formal change impact analyses for emulated control software
No full textProcessor emulators are a software tool for allowing legacy computer programs to be executed on a modern processor. In the past emulators have been used in trivial applications such as maintenance of video games. Now, however, processor emulation is being applied to safety-critical control systems, including military avionics. These applications demand utmost guarantees of correctness, but no verification techniques exist for proving that an emulated system preserves the original system’s functional and timing properties. Here we show how this can be done by combining concepts previously used for reasoning about real-time program compilation, coupled with an understanding of the new and old software architectures. In particular, we show how both the old and new systems can be given a common semantics, thus allowing their behaviours to be compared directly
Dispelling the Myths Behind First-author Citation Counts
No full textWe conducted a full-scale evaluative citation analysis study of scholars in the XML research field to explore just how different from each other author rankings resulting from different citation counting methods actually are, and to demonstrate the capability of emerging data and tools on the Web in supporting more realistic citation counting methods. Our results contest some common arguments for the continued
use of first-author citation counts in the evaluation of scholars, such as high correlations between author rankings by first-author citation counts and other citation
counting methods, and high costs of using more realistic citation counting methods that are not well-supported by the ISI databases. It is argued that increasingly available digital full text research papers make it possible for citation analysis studies to go beyond what the ISI databases have directly supported and to employ more
sophisticated methods
Model checking interrupt-dependent software
No full textEmbedded control programs are hard to analyse because their behaviour depends on how they interact with hardware devices. In particular, embedded code typically uses interrupts to respond to external events in a timely manner. Such asynchronous control constructs make static analysis difficult due to the potentially large number of alternative control-flow paths they allow. We show how model checking can be used to effectively analyse the behaviour of interrupt-dependent programs. This is done by developing an abstraction of the code that captures its essential timing and functional properties, including those related to external interrupts. The model is made efficient by grouping program instructions into basic blocks whose behaviour is atomic with respect to interrupts
- …
