Prof. Scott A. Smolka

My current research focuses on concurrency theory, particularly as it relates to model checking and the computer-aided verification of safety critical systems and biological systems. I am also interested in mobile-code and its impact on computer system security. I am currently performing federally funded research in the following areas:

The EHA (Excitable Hybrid Automata) project focuses on the use of Hybrid automata to model and analyze excitable cells such as cardiac cells and neurons. Hybrid automata are an increasingly popular modeling formalism for systems that exhibit both continuous and discrete behavior. They are well suited as a computational model for continuous-discrete systems as they (i) possess an intuitive graphical representation; (ii) can be used in a natural way to achieve a piecewise, possibly linear, approximation of any nonlinear system; and (iii) facilitate formal analysis due to their automata-theoretic nature.

In a collection of papers spanning the period 2005-2008 and culminating in a 2008 Journal of IET Systems Biology paper, We have shown how Hybrid Automata (HA) can be used to efficiently capture the behavior of excitable cells (e.g. neural and cardiac) previously modeled by complex systems of nonlinear differential equations. Their much simpler HA models are able to successfully capture the action-potential morphology of the different cells, as well as reproduce typical excitable cell characteristics, such as refractoriness (period of non-responsiveness to external stimulation) and restitution (adaptation to pacing rates). To model electrical wave propagation in a cell network, the single-cell HA models are linked to a classical 2D spatial model. The resulting simulation framework exhibits significantly improved computational efficiency in modeling complex wave patterns, such as the spiral waves underlying pathological conditions in the heart. The EHA project represents joint work with Prof. Radu Grosu of the Stony Brook Computer Science Department and Prof. Emilia Entcheva of the Stony Brook BioMedical Engineering Department. Funding for the EHA project has been provided by the NSF.

The Concurrency Factory design environment serves as the umbrella project for my research in computer-aided verification, in the sense that all theoretical developments are carried out with goal of eventually being implemented and applied in the Factory. The Concurrency Factory is a visual environment that allows protocol engineers, embedded-systems engineers, and software developers to specify, design, simulate, analyze, and implement concurrent systems. It is written in C++ in a highly object-oriented manner and uses Bell Lab's I-TCL/TK as the graphical engine for the visualization component. Care has been taken to make the implementation of the Factory as efficient as possible, so that it will be suitable for industrial applications. The Concurrency Factory is a joint project with Professor Rance Cleaveland and has been funded by the NSF, AFOSR, and ARO.

The aim of the LMC project (Logic-based Model Checking) is to utilize the Stony Brook XSB tabled logic programming system to attain an efficient and flexible modeling and verification environment. The research has so far produced two publically available verification environments: the XMC model checker for a very expressive value-passing process description language; and MMC, a verification tool for mobile systems described in the pi calculus. The LMC project is joint work with C.R. Ramakrishnan, I.V. Ramakrishnan, and David S. Warren and has been funded primarily by the NSF.

The Concurrency Factory's model-checking facility and the XMC model checker have recently been applied to several real-world systems, including the GNU UUCP i-protocol, the RETHER real-time ethernet protocol; the Display-LAN protocol of the Northrop Grumman Hawkeye Early Warning Aircraft; the Java meta-locking algorithm for ensuring mutually exclusive access by threads to object monitor queues; and a combined encryption and digital signature security protocol. Our experience shows that model checking can be used to find hard-to-detect errors that testing alone is unlikely uncover, or to discover interesting design alternatives.

We are also interested in attaining a modeling and verification environment capable of expressing stochastic or probabilistic behavior. For example, one might like to show that a certain communication network delivers at least 5 messages per second with a probability between 0.945 and 0.955. Our approach is based on Probabilistic I/O Automata (PIOA), and we have recently devised an efficient compositional approach to computing expected delays in networks of PIOA and implemented it as the PIOATool. The PIOA research is joint work with Professors Gene Stark and Rance Cleaveland and has been funded by the NSF and the ARO.

In research funded by the Army Research Office (ARO) under the supervision of David Hislop of the ARO, we are integrating the PIOATool into the Concurrency Workbench verification system developed by Rance Cleaveland and his students.

We are also interested in the rapid protoyping of systems via automatic code generation. In joint work with Rance Cleaveland and David Hansel of Reactive Systems, Inc., we have implemented a code generator for the Concurrency Workbench that produces efficient, fully distributed C++ code from formal specifications. The generated code utilizes Douglas C. Schmidt's ACE (ADAPTIVE Communication Environment) network programming interface for maximal protability to differrent distributed/concurrent execution environments.

In other research, the MCC (Model Carrying Code) project with Professors R. Sekar, C.R. Ramakrishnan, and I.V. Ramakrishnan explores how the security of mobile code can be enhanced by equipping mobile code with a model of the code's security-relevant behavior. A consumer of the mobile code can then validate the model for adherence to those security policies of interest to the consumer and use the model as the basis for runtime code monitoring and enforcement. The MCC project is supported by a CIP (Critical Infrastructure Program) award from the Office of Naval Research (ONR), Frank Deckelman, program manager.

We recently received an NSF ITR (Information Technology Research) award to study the use of formal techniques and runtime monitoring to uncover security vulnerabilities in computer systems. This is joint research with C.R. Ramakrishnan, I.V. Ramakrishnan, R. Sekar, and Scott Stoller.

My research in computer-aided verification is in the process of being transfered to industry through the company Reactive Systems, Inc (www.reactive-systems.com). RSI was founded in 1999 and is the recipient of Phase I and Phase II SBIR awards from the National Science Foundation. The principals of the company are myself (President), Rance Cleaveland (CEO), and Steve Sims (Chief Technology Officer). RSI makes design automation tools for embedded software. Its first product, released in June 2002, is the Reactis product suite which includes Reactis Tester, an automatic test-case generator for models of embedded software given in the market-leading Simulink/Stateflow modeling notation; Reactis Simulator, a visual simulator for such models; and Reactis Validator, which, given a Simulink/Stateflow model, checks the validy of user-specified requirements against the model. Simulink and Stateflow (registered trademarks of The Mathworks, Inc.) are widely used modeling notations for embedded software in industries as diverse as automotive, medical-device, and avionics. Customers so far include eight major automotive companies and one aerospace firm, with trails underway in more than a dozen other companies.