
Jee, Eunkyoung; Kim, Suin; Cha, Sungdeok; Lee, Insup
We present FBDTestMeasurer, an automated test coverage measurement tool for function block diagram (FBD) programs which are increasingly used in implementing safety critical systems such as nuclear reactor protection systems. We have defined new structural test coverage criteria for FBD programs in which dataflowcentric characteristics of FBD programs were well reflected. Given an FBD program and a set of test cases, FBDTestMeasurer produces test coverage score and uncovered test requirements with respect to the selected coverage criteria. Visual representation of uncovered data paths enables testers to easily identify which parts of the program need to be tested further. We found...

Wang, Anduo; Jia, Limin; Liu, Changbin; Loo, Boon Thau; Sokolsky, Oleg; Basu, Prithwish
This paper proposes Formally Verifiable Networking (FVN), a novel approach towards unifying the design, specification, implementation, and verification of networking protocols within a logicbased framework. In FVN, formal logical statements are used to specify the behavior and the properties of the protocol. FVN uses declarative networking as an intermediary layer between highlevel logical specifications of the network model and lowlevel implementations. A theorem prover is used to statically verify the properties of declarative network protocols. Moreover, a property preserving translation exists for generating declarative networking implementations from verified formal specifications. We further demonstrate the possibility of designing and specifying wellbehaved...

Wang, Shaohui; Ayoub, Anaheed; Sokolsky, Oleg; Lee, Insup
We present an online algorithm for the runtime checking of temporal properties, expressed as pasttime Linear Temporal Logic (LTL) over the traces of observations recorded by a "black box"like device. The recorder captures the observed values but not the precise time of their occurrences, and precise truth evaluation of a temporal logic formula cannot always be obtained. In order to handle this uncertainty, the checking algorithm is based on a threevalued semantics for pasttime LTL defined in this paper. In addition to the algorithm, the paper presents results of an evaluation that aimed to study the effects of the recording...

Dinesh, Nikhil; Joshi, Aravind; Lee, Insup; Sokolsky, Oleg
Formal languages for policy have been developed for access control and conformance checking. In this paper, we describe a formalism that combines features that have been developed for each application. From access control, we adopt the use of a saying operator. From conformance checking, we adopt the use of operators for obligation and permission. The operators are combined using an axiom that permits a principal to speak on behalf of another. The combination yields benefits to both applications. For access control, we overcome the problematic interaction between handoff and classical reasoning. For conformance, we obtain a characterization of legal power...

SERNIAKCATUDAL, DONNA
Rudolf Carnap's The Logical Structure of The World (Aufbau) remains the most sustained and detailed attempt to convert logicomathematical procedures to use in empirical and scientific discourse. Moreover, the failure of Carnap's attempts to apply logic to empirical and scientific discourse is central to the legacy of metaphysical projects and epistemological programs that constitutes Contemporary Analytic philosophy.^ Contemporary assessments of logical positivism identify Carnap's Aufbau endeavors as empiricist in conception by focussing on the verification and testability of empirical and scientific theories. I argue for a Kantian interpretation of the Aufbau, and thereby offer a different picture of Carnap's conception...

Baumard, Nicolas; Mascaro, Olivier; Chevallier, Coralie
Classic studies in developmental psychology demonstrate a relatively late development of equity, with children as old as 6 or even 8–10 years failing to follow the logic of merit—that is, giving more to those who contributed more. Following Piaget (1932), these studies have been taken to indicate that judgments of justice develop slowly and follow a stagelike progression, starting off with simple rules (e.g., equality: everyone receives the same) and only later on in development evolving into more complex ones (e.g., equity: distributions match contributions). Here, we report 2 experiments with 3 and 4yearold children (N = 195) that contradict...

Alur, Rajeev; Deshmukh, Jyotirmoy; MadorHaim, Sela; Martin, Milo; Raghavan, Arun; Udupa, Abhishek
With the maturing of computeraided verification technology, there is an emerging opportunity to develop design tools that can transform the way systems are designed. In this paper, we propose a new way to specify protocols using concolic snippets, that is, sample execution fragments that contain both concrete and symbolic values. While the purely symbolic extreme is simply an alternative representation of the traditional communicating extended finitestatemachines, and the purely concrete extreme is an instantiation of the "programming by examples" paradigm, our specification language allows the designer to specify the desired protocol using a mixture of symbolic state machines and concrete...

Partzsch, Henriette
Faustina Sáez de Melgar (18341895) fue una escritora comercial, de éxito innegable en el mundo hispanohablante de la segunda mitad del siglo XIX. Estas dos afirmaciones traen consigo casi automáticamente una tercera: junto con algunas de sus compañeras de generación, como Pilar Sinués de Marco, la autora ocupa un lugar problemático en la historia de la literatura. Parece que nos sigue produciendo un cierto malestar pensar en la expansión de la cultura literaria de la mano de la lógica capitalista, que se va acelerando en el siglo XIX para finalmente alcanzar los últimos rincones del mundo actual. Nuestro gusto literario...

Alur, Rajeev; Arenas, Marcelo; Barcelo, Pablo; Etessami, Kousha; Immerman, Neil; Libkin, Leonid
Nested words are a structured model of execution paths in procedural programs, reflecting their call and return nesting structure. Finite nested words also capture the structure of parse trees and other treestructured data, such as XML. We provide new temporal logics for finite and infinite nested words, which are natural extensions of LTL, and prove that these logics are firstorder expressivelycomplete. One of them is based on adding a "within" modality, evaluating a formula on a subword, to a logic CaRet previously studied in the context of verifying properties of recursive state machines (RSMs). The other logic, NWTL, is based...

Alur, Rajeev; Weiss, Gera
We present a framework for componentbased design and scheduling of realtime embedded software. Each component has a clearly specified interface that includes the methods used for sensing, computation, and actuation, along with a requirement given as a regular set of macroschedules. Each macroschedule is an infinite sequence that specifies, for every time slot, the set of component methods invoked in that slot. The macroscheduler composes the specifications of all the components, along with the platform specification that constrains which methods can be executed within a single slot, to generate a feasible macroschedule. Within a slot, we use logical execution time...

Alur, Rajeev; Filiot, Emmanuel; Trivedi, Ashutosh
The theory of regular transformations of finite strings is quite mature with appealing properties. This class can be equivalently defined using both logic (Monadic secondorder logic) and finitestate machines (twoway transducers, and more recently, streaming string transducers); is closed under operations such as sequential composition and regular choice; and problems such as functional equivalence and type checking, are decidable for this class. In this paper, we initiate a study of transformations of infinite strings. The MSObased definition for regular string transformations generalizes naturally to infinite strings. We define an equivalent generalization of the machine model of streaming string transducers to...

Alur, Rajeev; Madhusudan, P.
We propose the model of nested words for representation of data with both a linear ordering and a hierarchically nested matching of items. Examples of data with such dual linearhierarchical structure include executions of structured programs, annotated linguistic data, and HTML/XML documents. Nested words generalize both words and ordered trees, and allow both word and tree operations. We define nested word automata—finitestate acceptors for nested words, and show that the resulting class of regular languages of nested words has all the appealing theoretical properties that the classical regular word languages enjoys: deterministic nested word automata are as expressive as their...

Alur, Rajeev; D'Antoni, Loris
Theory of tree transducers provides a foundation for understanding expressiveness and complexity of analysis problems for specification languages for transforming hierarchically structured data such as XML documents. We introduce streaming tree transducers as an analyzable, executable, and expressive model for transforming unranked ordered trees (and hedges) in a single pass. Given a linear encoding of the input tree, the transducer makes a single lefttoright pass through the input, and computes the output in linear time using a finitestate control, a visibly pushdown stack, and a finite number of variables that store output chunks that can be combined using the operations...

Alur, Rajeev; Chaudhuri, Swarat; Madhusudan, P.
We study languages of nested trees—structures obtained by augmenting trees with sets of nested jumpedges. These graphs can naturally model branching behaviors of pushdown programs, so that the problem of branchingtime software model checking may be phrased as a membership question for such languages. We define finitestate automata accepting such languages—these automata can pass states along jumpedges as well as tree edges. We find that the modelchecking problem for these automata on pushdown systems is EXPTIMEcomplete, and that their alternating versions are expressively equivalent to NTμ, a recently proposed temporal logic for nested trees that can express a variety of...

Alur, Rajeev; Chaudhuri, Swarat; Madhusudan, P.
We define a new fixpoint modal logic, the visibly pushdown μcalculus (VPμ), as an extension of the modal μcalculus. The models of this logic are execution trees of structured programs where the procedure calls and returns are made visible. This new logic can express pushdown specifications on the model that its classical counterpart cannot, and is motivated by recent work on visibly pushdown languages [4]. We show that our logic naturally captures several interesting program specifications in program verification and dataflow analysis. This includes a variety of program specifications such as computing combinations of local and global program flows, pre/post...

Wabiszewski, Graham E.
Energy consumption by computers and electronics is currently 15% of worldwide energy output, and growing. Aggressive scaling of the fullyelectronic transistor, which is the fundamental computational element of these devices, has led to significant and immutable energy losses. Ohmic nanoelectromechanical systems (NEMS) logic switches have been recognized as a potential transistor replacement technology with projected energy savings of one to three orders of magnitude over traditional, fullyelectronic transistors. However, the use of conventional, adhesive contact materials (i.e. metals) in NEMS switches electrical contacts leads to permanent device seizure or the formation of insulating tribofilms that inhibits commercialization of this technology....

Roodhouse, Elizabeth
Academics, marketers, and the general public share a growing interest in socially conscious products that claim to support (or oppose) a variety of causes and issues, from protecting the environment to objecting to free trade agreements between countries. Although the presence of such products has grown both in the US and abroad, both academics and marketers assume that niche audiences haveand will continue toconsume the vast majority of socially conscious products. This logic implies that socially conscious products have limited political impact due to their constrained market share, and that socially conscious consumption is a generic behavior similar to "volunteering"...

Porter, Dot
http://repository.upenn.edu/sims_video/1035/thumbnail.jpg

Mazurak, Karl
Session types and typestate both promise a type system that can reason about protocol
adherence. The complexity budgets of most programming languages, however, do not
allow for new forms of types aimed at specific problem domainseven domains as broad
as these.
Classical F◦ read "Fpop"is a typed λcalculus based on classical (i.e., full) linear
logic, wherein session types arise naturally from the interaction between the usual sums,
products, and implications of linear logic and a simple process model, with the dualizing
negation of classical logic naturally accounting for how a protocol is seen by each of a
channel's endpoints. Classical F◦ expressions evaluate to processes, reminiscent of those
in...

Alur, Rajeev
Model checking is emerging as a practical tool for automated debugging of complex reactive systems such as embedded controllers and network protocols (see[CK96] for a survey). In model checking, a high level description of a system is compared against a logical correctness requirement to discover inconsistencies. Traditional techniques for model checking do not admit an explicit modeling of time, and are thus, unsuitable for analysis of realtime systems whose correctness depends on relative magnitudes of different delays. Consequently, timed automata [AD94] were introduced as a formal notation to model the behavior of realtime systems. Its definition provides a simple, and...