Search For:

Displaying 1-30 out of 30 total
Software monitoring with bounded overhead
Found in: Parallel and Distributed Processing Symposium, International
By Sean Callanan, Daniel J. Dean, Michael Gorbovitski, Radu Grosu, Justin Seyster, Scott A. Smolka, Scott D. Stoller, Erez Zadok
Issue Date:April 2008
pp. 1-8
In this paper, we introduce the new technique of High-Confidence Software Monitoring (HCSM), which allows one to perform software monitoring with bounded overhead and concomitantly achieve high confidence in the observed error rates. HCSM is formally groun...
 
Stochastic Game-Based Analysis of the DNS Bandwidth Amplification Attack Using Probabilistic Model Checking
Found in: 2014 Tenth European Dependable Computing Conference (EDCC)
By Tushar Deshpande,Panagiotis Katsaros,Scott A. Smolka,Scott D. Stoller
Issue Date:May 2014
pp. 226-237
The Domain Name System (DNS) is an Internet-wide, hierarchical naming system used to translate domain names into numeric IP addresses. Any disruption of DNS service can have serious consequences. We present a formal game-theoretic analysis of a notable thr...
 
Automated Software Engineering Using Concurrent Class Machines
Found in: Automated Software Engineering, International Conference on
By Radu Grosu, Yanhong A. Liu, Scott Smolka, Scott D. Stoller, Jingyu Yan
Issue Date:November 2001
pp. 297
Concurrent Class Machines are a novel state-machine model that directly captures a variety of object-oriented concepts, including classes and inheritance, objects and object creation, methods, method invocation and exceptions, multithreading and abstract c...
 
Learning and detecting emergent behavior in networks of cardiac myocytes
Found in: Communications of the ACM
By Anita Wasilewska, Emilia Entcheva, Ezio Bartocci, Flavio Corradini, Radu Grosu, Scott A. Smolka, Anita Wasilewska, Emilia Entcheva, Ezio Bartocci, Flavio Corradini, Radu Grosu, Scott A. Smolka
Issue Date:March 2009
pp. 101-104
We address the problem of specifying and detecting emergent behavior in networks of cardiac myocytes, spiral electric waves in particular, a precursor to atrial and ventricular fibrillation. To solve this problem we: (1) apply discrete mode abstraction to ...
     
Curvature Analysis of Cardiac Excitation Wavefronts
Found in: IEEE/ACM Transactions on Computational Biology and Bioinformatics
By Abhishek Murthy,Ezio Bartocci,Flavio H. Fenton,James Glimm,Richard A. Gray,Elizabeth M. Cherry,Scott A. Smolka,Radu Grosu
Issue Date:March 2013
pp. 323-336
We present the Spiral Classification Algorithm (SCA), a fast and accurate algorithm for classifying electrical spiral waves and their associated breakup in cardiac tissues. The classification performed by SCA is an essential component of the detection and ...
 
Formal Analysis of the DNS Bandwidth Amplification Attack and Its Countermeasures Using Probabilistic Model Checking
Found in: High-Assurance Systems Engineering, IEEE International Symposium on
By Tushar Deshpande,Panagiotis Katsaros,Stylianos Basagiannis,Scott A. Smolka
Issue Date:November 2011
pp. 360-367
The DNS Bandwidth Amplification Attack (BAA) is a distributed denial-of-service attack in which a network of computers floods a DNS server with responses to requests that have never been made. Amplification enters into the attack by virtue of the fact that...
 
Formal Analysis of the Kaminsky DNS Cache-Poisoning Attack Using Probabilistic Model Checking
Found in: High-Assurance Systems Engineering, IEEE International Symposium on
By Nikolaos Alexiou, Stylianos Basagiannis, Panagiotis Katsaros, Tushar Dashpande, Scott A. Smolka
Issue Date:November 2010
pp. 94-103
We use the probabilistic model checker PRISM to formally model and analyze the highly publicized Kaminsky DNS cache-poisoning attack. DNS (Domain Name System) is an internet-wide, hierarchical naming system used to translate domain names such as google.com...
 
Power Optimization in Fault-Tolerant Mobile Ad Hoc Networks
Found in: High-Assurance Systems Engineering, IEEE International Symposium on
By Oliviero Riganelli, Radu Grosu, Samir R. Das, C.R. Ramakrishnan, Scott A. Smolka
Issue Date:December 2008
pp. 362-370
In this paper, we investigate the transmission-power assignment problem for k-connected Mobile Ad hoc NETworks (MANETs), the problem of optimizing the lifetime of a MANET at a given degree k of connectivity by minimizing power consumption. Our proposed sol...
 
Model Predictive Control for Memory Profiling
Found in: Parallel and Distributed Processing Symposium, International
By Sean Callanan, Radu Grosu, Justin Seyster, Scott A. Smolka, Erez Zadok
Issue Date:March 2007
pp. 324
We make two contributions in the area of memory profiling. The first is a real-time, memory-profiling toolkit we call Memcov that provides both allocation/deallocation and access profiles of a running program. Memcov requires no recompilation or relinking ...
 
Safety-Liveness Semantics for UML 2.0 Sequence Diagrams
Found in: Application of Concurrency to System Design, International Conference on
By Radu Grosu, Scott A. Smolka
Issue Date:June 2005
pp. 6-14
We provide an automata-theoretic solution to one of the main open questions about the UML standard, namely how to assign a formal semantics to a set of sequence diagrams without compromising refinement? Our solution relies on a rather obvious idea, but to ...
 
Model Checking and Evidence Exploration
Found in: Engineering of Computer-Based Systems, IEEE International Conference on the
By Yifei Dong, C. R. Ramakrishnan, Scott A. Smolka
Issue Date:April 2003
pp. 214
We present an algebraic framework for evidence exploration: the process of interpreting, manipulating, and navigating the proof structure or evidence produced by a model checker when attempting to verify a system specification for a temporal-logic property...
 
Distributed Prototyping from Validated Specifications
Found in: Rapid System Prototyping, IEEE International Workshop on
By David Hansel, Rance Cleaveland, Scott A. Smolka
Issue Date:June 2001
pp. 0097
Abstract: We present vpl2cxx, a translator that automatically generates efficient, fully distributed C++ code from high-level system designs specified in the mathematically rigorous VPL design language. The Concurrency Workbench of the New Century (CWB-NC)...
 
Model Checking the Java Meta-Locking Algorithm
Found in: Engineering of Computer-Based Systems, IEEE International Conference on the
By Samik Basu, Scott A. Smolka, Orson R. Ward
Issue Date:April 2000
pp. 342
We apply the XMC model checker to the Java meta-locking algorithm, a highly optimized technique for ensuring mutually exclusive access by threads to object monitor queues. Our abstract specification of the meta-locking algorithm is fully parameterized, bot...
 
Practical Considerations in Protocol Verification: The E-2C Case Study
Found in: Engineering of Complex Computer Systems, IEEE International Conference on
By Yifei Dong, Scott A. Smolka, Eugene W. Stark, Stephanie M. White
Issue Date:October 1999
pp. 153
We report on our efforts to formally specify and verify a new protocol of the E-2C Hawkeye Early Warning Aircraft. The protocol, which is currently in test at Northrop Grumman, supports communication between a Mission Computer (MC) and three or more Tactic...
 
Model Checking the Secure Electronic Transaction (SET) Protocol
Found in: Modeling, Analysis, and Simulation of Computer Systems, International Symposium on
By Shiyong Lu, Scott A. Smolka
Issue Date:March 1999
pp. 358
We use model checking to establish five essential correctness properties of the Secure Electronic Transaction (SET) protocol. SET has been developed jointly by Visa and MasterCard as a method to secure payment card transactions over open networks, and indu...
 
Strong Interaction Fairness Via Randomization
Found in: IEEE Transactions on Parallel and Distributed Systems
By Yuh-Jzer Joung, Scott A. Smolka
Issue Date:February 1998
pp. 137-149
<p><b>Abstract</b>—We present M<scp>ULTI</scp>, a symmetric, distributed, randomized algorithm that, with probability one, schedules multiparty interactions in a strongly fair manner. To our knowledge, M<scp>ULTI</scp...
 
On the energy consumption and performance of systems software
Found in: Proceedings of the 4th Annual International Conference on Systems and Storage (SYSTOR '11)
By Erez Zadok, Priya Sehgal, Radu Grosu, Scott A. Smolka, Scott D. Stoller, Zhichao Li
Issue Date:May 2011
pp. 1-12
Models of energy consumption and performance are necessary to understand and identify system behavior, prior to designing advanced controls that can balance out performance and energy use. This paper considers the energy consumption and performance of serv...
     
Tabled Resolution + Constraints: A Recipe for Model Checking Real-Time Systems
Found in: Real-Time Systems Symposium, IEEE International
By Xiaoqun Du, C. R. Ramakrishnan, Scott A. Smolka
Issue Date:November 2000
pp. 175
We present a computational framework based on tabled resolution and constraint processing for verifying real-time systems. We also discuss the implementation of this frame-work in the context of the XMC/RT verification tool. For systems specified using tim...
 
Curvature Analysis of Cardiac Excitation Wavefronts
Found in: IEEE/ACM Transactions on Computational Biology and Bioinformatics (TCBB)
By Abhishek Murthy, Elizabeth M. Cherry, Ezio Bartocci, Flavio H. Fenton, James Glimm, Radu Grosu, Richard A. Gray, Scott A. Smolka
Issue Date:March 2013
pp. 323-336
We present the Spiral Classification Algorithm (SCA), a fast and accurate algorithm for classifying electrical spiral waves and their associated breakup in cardiac tissues. The classification performed by SCA is an essential component of the detection and ...
     
On the computational complexity of bisimulation, redux
Found in: Proceedings of the Paris C. Kanellakis memorial workshop on Principles of computing & knowledge: Paris C. Kanellakis memorial workshop on the occasion of his 50th birthday (PCK50)
By Faron Moller, Scott A. Smolka
Issue Date:June 2003
pp. 55-59
Constraint Databases (CDBs) are an extension of relational databases that enrich both the relational data model and the relational query primitives with constraints. By providing a finite representation of data with infinite semantics, the Constraint Datab...
     
High-confidence operating systems
Found in: Proceedings of the 10th workshop on ACM SIGOPS European workshop: beyond the PC (EW10)
By Erez Zadok, Radu Grosu, Rance Cleaveland, Scott A. Smolka, Yanhong A. Liu
Issue Date:July 2002
pp. 205-208
Operating systems (OSs) are among the most sophisticated software systems in widespread use, and among the most expensive and time-consuming to develop and maintain. OS software must also be robust and dependable, since OS failures can result in system cra...
     
A comprehensive study of the complexity of multiparty interaction
Found in: Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '92)
By Scott A. Smolka, Yuh-Jzer Joung
Issue Date:January 1992
pp. 142-153
We present a taxonomy of languages for multiparty interaction, which covers all proposals of which we are aware. Based on this taxonomy, we present a comprehensive analysis of the computational complexity of the multiparty interaction implementation proble...
     
Concurrency: theory and practice
Found in: ACM Computing Surveys (CSUR)
By Rocco De Nicola, Scott A. Smolka
Issue Date:March 1988
pp. 52-es
Floating-point divide and square-root operations are essential to many scientific and engineering applications, and are required in all computer systems that support the IEEE floating-point standard. Yet many current microprocessors provide only weak supp...
     
Strategic directions in concurrency research
Found in: ACM Computing Surveys (CSUR)
By Rance Cleaveland, Scott A. Smolka
Issue Date:March 1988
pp. 607-625
Floating-point divide and square-root operations are essential to many scientific and engineering applications, and are required in all computer systems that support the IEEE floating-point standard. Yet many current microprocessors provide only weak supp...
     
On the computational complexity of bisimulation
Found in: ACM Computing Surveys (CSUR)
By Faron Moller, Scott A. Smolka
Issue Date:March 1988
pp. 287-289
A multidatabase system (MDBS) is a confederation of preexisting distributed, heterogeneous, and autonomous database systems. There has been a recent proliferation of research suggesting the application of object-oriented techniques to facilitate the comple...
     
On randomization in sequential and distributed algorithms
Found in: ACM Computing Surveys (CSUR)
By Rajiv Gupta, Scott A. Smolka, Shaji Bhaskar
Issue Date:March 1988
pp. 7-86
Probabilistic, or randomized, algorithms are fast becoming as commonplace as conventional deterministic algorithms. This survey presents five techniques that have been widely used in the design of randomized algorithms. These techniques are illustrated usi...
     
Coordinating first-order multiparty interactions
Found in: ACM Transactions on Programming Languages and Systems (TOPLAS)
By Scott A. Smolka, Yuh-Jzer Joung
Issue Date:January 1988
pp. 954-985
A first-order multiparty interaction is an abstraction mechanism that defines communication among a set of formal process roles. Actual processes participate in a first-order interaction by enroling into roles, and execution of the interaction can proceed ...
     
A comprehensive study of the complexity of multiparty interaction
Found in: Journal of the ACM (JACM)
By Scott A. Smolka, Yuh-Jzer Joung
Issue Date:January 1988
pp. 75-115
SLD resolution with negation as finite failure (SLDNF) reflects the procedural interpretation of predicate calculus as a programming language and forms the computational basis for Prolog systems. Despite its advantages for stack-based memory management, SL...
     
On the analysis of cooperation and antagonism in networks of communicating processes
Found in: Proceedings of the fourth annual ACM symposium on Principles of distributed computing (PODC '85)
By Paris C. Kanellakis, Scott A. Smolka
Issue Date:August 1985
pp. 23-38
An efficient distributed algorithm to detect deadlocks in distributed and dynamically changing systems is presented. In our model, processes can request any N available resources from a pool of size M. This is a generalization of the well-known AND-OR requ...
     
CCS expressions, finite state processes, and three problems of equivalence
Found in: Proceedings of the second annual ACM symposium on Principles of distributed computing (PODC '83)
By Paris C. Kanellakis, Scott A. Smolka
Issue Date:August 1983
pp. 228-240
We examine the computational complexity of testing finite state processes for equivalence, in the Calculus of Communicating Systems (CCS). This equivalence problem in CCS is presented as a refinement of the familiar problem of testing whether two nondeterm...
     
 1