Search For:

Displaying 1-41 out of 41 total
Analyzing Conversations of Web Services
Found in: IEEE Internet Computing
By Tevfik Bultan, Jianwen Su, Xiang Fu
Issue Date:January 2006
pp. 18-25
A conversation is the global sequence of messages exchanged among the components of a distributed system. Conversations provide a promising model for specifying and analyzing the interactions among the peers participating to a composite Web service. In thi...
 
Modular Verification of Asynchronous Service Interactions Using Behavioral Interfaces
Found in: IEEE Transactions on Services Computing
By Aysu Betin-Can,Sylvain Halle,Tevfik Bultan
Issue Date:April 2013
pp. 262-275
A crucial problem in service-oriented computing is the specification and analysis of interactions among multiple peers that communicate via messages. We propose a design pattern that enables the specification of behavioral interfaces acting as communicatio...
 
Realizability of Choreographies Using Process Algebra Encodings
Found in: IEEE Transactions on Services Computing
By Gwen Salaün,Tevfik Bultan,Nima Roohi
Issue Date:July 2012
pp. 290-304
Service-oriented computing has emerged as a new software development paradigm that enables implementation of Web accessible software systems that are composed of distributed services which interact with each other via exchanging messages. Modeling and anal...
 
Runtime Verification of Web Service Interface Contracts
Found in: Computer
By Sylvain Hallé, Tevfik Bultan, Graham Hughes, Muath Alkhalaf, Roger Villemaire
Issue Date:March 2010
pp. 59-66
Experiments with the Amazon E-Commerce Service demonstrate the advantages of using a model-based approach for the runtime testing and monitoring of Web applications.
 
Generating Vulnerability Signatures for String Manipulating Programs Using Automata-Based Forward and Backward Symbolic Analyses
Found in: Automated Software Engineering, International Conference on
By Fang Yu, Muath Alkhalaf, Tevfik Bultan
Issue Date:November 2009
pp. 605-609
Given a program and an attack pattern (specified as a regular expression), we automatically generate string-based vulnerability signatures, i.e., a characterization that includes all malicious inputs that can be used to generate attacks. We use an automata...
 
A Tool for Choreography Analysis Using Collaboration Diagrams
Found in: Web Services, IEEE International Conference on
By Tevfik Bultan, Chris Ferguson, Xiang Fu
Issue Date:July 2009
pp. 856-863
Analyzing interactions among peers that interact via messages is a crucial problem due to increasingly distributed nature of current software systems, especially the ones built using the service oriented computing paradigm. In service oriented computing, i...
 
Interface Grammars for Modular Software Model Checking
Found in: IEEE Transactions on Software Engineering
By Graham Hughes,Tevfik Bultan
Issue Date:September 2008
pp. 614-632
Verification techniques relying on state enumeration (e.g., model checking) face two important challenges: the state-space explosion, an exponential increase in the state space as the number of components increases; and environment generation, modeling com...
 
Specification of Realizable Service Conversations Using Collaboration Diagrams
Found in: Service-Oriented Computing and Applications, IEEE International Conference on
By Tevfik Bultan, Xiang Fu
Issue Date:June 2007
pp. 122-132
Specification, modeling and analysis of interactions among peers that communicate via messages are becoming increasingly important due to the emergence of service oriented computing. Collaboration diagrams provide a convenient visual model for specifying s...
 
Modeling Interactions of Web Software
Found in: Automated Specification and Verification of Web Systems, International Workshop on
By Tevfik Bultan
Issue Date:November 2006
pp. 45-52
Modeling interactions among software components is becoming increasingly important for analyzing behavior of web software. This is especially true for the area of web services where distributed interactions across organizational boundaries are the norm. In...
 
Synchronizability of Conversations among Web Services
Found in: IEEE Transactions on Software Engineering
By Xiang Fu, Tevfik Bultan, Jianwen Su
Issue Date:December 2005
pp. 1042-1055
We present a framework for analyzing interactions among Web services that communicate with asynchronous messages. We model the interactions among the peers participating in a composite Web service as conversations, the global sequences of messages exchange...
 
Verifiable Web Services with Hierarchical Interfaces
Found in: Web Services, IEEE International Conference on
By Aysu Betin-Can, Tevfik Bultan
Issue Date:July 2005
pp. 85-94
We propose an Hierarchical StateMachine (HSM) model for specifying behavioral interfaces of peers participating in a composite web service. We integrate the HSM model to a design pattern which is supported by a modular verification technique that can 1) st...
 
Verifiable Concurrent Programming Using Concurrency Controllers
Found in: Automated Software Engineering, International Conference on
By Aysu Betin-Can, Tevfik Bultan
Issue Date:September 2004
pp. 248-257
We present a framework for verifiable concurrent programming in Java based on a design pattern for concurrency controllers. Using this pattern, a programmer can write concurrency controller classes defining a synchronization policy by specifying a set of g...
 
Realizability of Conversation Protocols With Message Contents
Found in: Web Services, IEEE International Conference on
By Xiang Fu, Tevfik Bultan, Jianwen Su
Issue Date:June 2004
pp. 96
A conversation protocol is a top-down specification framework which specifies desired global behaviors of a web service composition. In our earlier work [A formalism for specification and verification of reactive electronic services] we studied the problem...
 
Action Language Verifier
Found in: Automated Software Engineering, International Conference on
By Tevfik Bultan, Tuba Yavuz-Kahveci
Issue Date:November 2001
pp. 382
Action Language is a specification language for reactive software systems. In this paper we present the Action Language Verifier which consists of 1) a compiler that converts Action Language specifications to composite symbolic representations, and 2) an i...
 
Automated Test Generation from Vulnerability Signatures
Found in: 2014 IEEE Seventh International Conference on Software Testing, Verification and Validation (ICST)
By Abdulbaki Aydin,Muath Alkhalaf,Tevfik Bultan
Issue Date:March 2014
pp. 193-202
Web applications need to validate and sanitize user inputs in order to avoid attacks such as Cross Site Scripting (XSS) and SQL Injection. Writing string manipulation code for input validation and sanitization is an error-prone process leading to many vuln...
 
Unbounded data model verification using SMT solvers
Found in: 2012 27th IEEE/ACM International Conference on Automated Software Engineering (ASE)
By Jaideep Nijjar,Tevfik Bultan
Issue Date:September 2012
pp. 210-219
The growing influence of web applications in every aspect of society makes their dependability an immense concern. A fundamental building block of web applications that use the Model-View-Controller (MVC) pattern is the data model, which specifies the obje...
 
Action Language: A Specification Language for Model Checking Reactive Systems
Found in: Software Engineering, International Conference on
By Tevfik Bultan
Issue Date:June 2000
pp. 335
We present a specification language called Action Language for model checking software specifications. Action Languae Forms an interface between transition system models that a model checker generates and high level specification languages such as Statecha...
 
Data model property inference and repair
Found in: Proceedings of the 2013 International Symposium on Software Testing and Analysis (ISSTA 2013)
By Jaideep Nijjar, Tevfik Bultan
Issue Date:July 2013
pp. 202-212
Nowadays many software applications are deployed over compute clouds using the three-tier architecture, where the persistent data for the application is stored in a backend datastore and is accessed and modified by the server-side code based on the user in...
     
Unbounded data model verification using SMT solvers
Found in: Proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering (ASE 2012)
By Jaideep Nijjar, Tevfik Bultan
Issue Date:September 2012
pp. 210-219
The growing influence of web applications in every aspect of society makes their dependability an immense concern. A fundamental building block of web applications that use the Model-View-Controller (MVC) pattern is the data model, which specifies the obje...
     
ViewPoints: differential string analysis for discovering client- and server-side input validation inconsistencies
Found in: Proceedings of the 2012 International Symposium on Software Testing and Analysis (ISSTA 2012)
By Alessandro Orso, Christopher Kruegel, Mattia Fazzini, Muath Alkhalaf, Shauvik Roy Choudhary, Tevfik Bultan
Issue Date:July 2012
pp. 56-66
Since web applications are easily accessible, and often store a large amount of sensitive user information, they are a common target for attackers. In particular, attacks that focus on input validation vulnerabilities are extremely effective and dangerous....
     
Deciding choreography realizability
Found in: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '12)
By Tevfik Bultan, Meriem Ouederni, Samik Basu
Issue Date:January 2012
pp. 226-235
Since software systems are becoming increasingly more concurrent and distributed, modeling and analysis of interactions among their components is a crucial problem. In several application domains, message-based communication is used as the interaction mech...
     
Bounded verification of Ruby on Rails data models
Found in: Proceedings of the 2011 International Symposium on Software Testing and Analysis (ISSTA '11)
By Jaideep Nijjar, Tevfik Bultan
Issue Date:July 2011
pp. 67-77
The use of scripting languages to build web applications has increased programmer productivity, but at the cost of degrading dependability. In this paper we focus on a class of bugs that appear in web applications that are built based on the Model-View-Con...
     
Patching vulnerabilities with sanitization synthesis
Found in: Proceeding of the 33rd international conference on Software engineering (ICSE '11)
By Fang Yu, Muath Alkhalaf, Tevfik Bultan
Issue Date:May 2011
pp. 251-260
We present automata-based static string analysis techniques that automatically generate sanitization statements for patching vulnerable web applications. Our approach consists of three phases: Given an attack pattern we first conduct a vulnerability analys...
     
Choreography conformance via synchronizability
Found in: Proceedings of the 20th international conference on World wide web (WWW '11)
By Samik Basu, Tevfik Bultan
Issue Date:March 2011
pp. 795-804
Choreography analysis has been a crucial problem in service oriented computing. Interactions among services involve message exchanges across organizational boundaries in a distributed computing environment, and in order to build such systems in a reliable ...
     
Software for everyone by everyone
Found in: Proceedings of the FSE/SDP workshop on Future of software engineering research (FoSER '10)
By Tevfik Bultan
Issue Date:November 2010
pp. 69-74
Given the dizzying pace of change in computer science, trying to look too far into the future of software engineering is hard. However, it might be possible to predict the future of software for the next decade based on the current trends. And based on the...
     
Analyzing singularity channel contracts
Found in: Proceedings of the eighteenth international symposium on Software testing and analysis (ISSTA '09)
By Tevfik Bultan, Zachary Stengel
Issue Date:July 2009
pp. 5-6
This paper presents techniques for analyzing channel contract specifications in Microsoft Research's Singularity operating system. A channel contract is a state machine that specifies the allowable interactions between a server and a client through an asyn...
     
Modular verification of web services using efficient symbolic encoding and summarization
Found in: Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering (SIGSOFT '08/FSE-16)
By Aarti Gupta, Chao Wang, Fang Yu, Tevfik Bultan
Issue Date:November 2008
pp. 1-2
We propose a novel method for modular verification of web service compositions. We first use symbolic fixpoint computations to derive conditions on the incoming messages and relations among the incoming and outgoing messages of individual BPEL web services...
     
Client and server verification for web services using interface grammars
Found in: Proceedings of the 2008 workshop on Testing, analysis, and verification of web services and applications (TAV-WEB '08)
By Graham Hughes, Muath Alkhalaf, Tevfik Bultan
Issue Date:July 2008
pp. 40-46
Web services provide a promising framework for developing interoperable software components that interact with each other across organizational boundaries. For this framework to be successful, the client and the server for a service have to interact with e...
     
Workshop on testing, analysis and verification of web software (TAV-WEB 2008)
Found in: Proceedings of the 2008 international symposium on Software testing and analysis (ISSTA '08)
By Tao Xie, Tevfik Bultan
Issue Date:July 2008
pp. 119-120
TAV-WEB 2008 is the third in a series of workshops that focus on testing, analysis and verification of web software. The goal of these workshops has been to bring together researchers from academic, research, and industrial communities interested in the em...
     
Extended interface grammars for automated stub generation
Found in: Proceedings of the second workshop on Automated formal methods (AFM '07)
By Graham Hughes, Tevfik Bultan
Issue Date:November 2007
pp. 41-50
An important challenge in software verification is the ability to verify different software components in isolation. Achieving modularity in software verification requires development of innovative interface specification languages. In this paper we focus ...
     
Automated size analysis for OCL
Found in: Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering (ESEC-FSE '07)
By Erik Peterson, Fang Yu, Tevfik Bultan
Issue Date:September 2007
pp. 331-340
An essential tool in object oriented modeling is the specification of cardinalities of associations between classes. In Object Constraint Language (OCL) such constraints are expressed as conditions on the sizes of the collections that correspond to associa...
     
Application of design for verification with concurrency controllers to air traffic control software
Found in: Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering (ASE '05)
By Aysu Betin-Can, Benjamin Lux, Mikael Lindvall, Stefan Topp, Tevfik Bultan
Issue Date:November 2005
pp. 14-23
We present an experimental study which demonstrates that model checking techniques can be effective in finding synchronization errors in safety critical software when they are combined with a design for verification approach. We apply the concurrency contr...
     
Design for verification for asynchronously communicating Web services
Found in: Proceedings of the 14th international conference on World Wide Web (WWW '05)
By Aysu Betin-Can, Tevfik Bultan, Xiang Fu
Issue Date:May 2005
pp. 750-759
We present a design for verification approach to developing reliable web services. We focus on composite web services which consist of asynchronously communicating peers. Our goal is to automatically verify properties of interactions among such peers. We p...
     
Model checking XML manipulating software
Found in: Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis (ISSTA '04)
By Jianwen Su, Tevfik Bultan, Xiang Fu
Issue Date:July 2004
pp. 231-231
The use of XML as the de facto data exchange standard has allowed integration of heterogeneous web based software systems regardless of implementation platforms and programming languages. On the other hand, the rich tree-structured data representation, and...
     
Conversation specification: a new approach to design and analysis of e-service composition
Found in: Proceedings of the twelfth international conference on World Wide Web (WWW '03)
By Jianwen Su, Richard Hull, Tevfik Bultan, Xiang Fu
Issue Date:May 2003
pp. 403-410
This paper introduces a framework for modeling and specifying the global behavior of e-service compositions. Under this framework, peers (individual e-services) communicate through asynchronous messages and each peer maintains a queue for incoming messages...
     
Specification, verification, and synthesis of concurrency control components
Found in: Proceedings of the international symposium on Software testing and analysis (ISSTA '02)
By Tevfik Bultan, Tuba Yavuz-Kahveci
Issue Date:July 2002
pp. 240
Run-time errors in concurrent programs are generally due to the wrong usage of synchronization primitives such as monitors. Conventional validation techniques such as testing become ineffective for concurrent programs since the state space increases expone...
     
Action Language: a specification language for model checking reactive systems
Found in: Proceedings of the 22nd international conference on Software engineering (ICSE '00)
By Tevfik Bultan
Issue Date:June 2000
pp. 335-344
We present a specification language called Action Language for model checking software specifications. Action Language forms an interface between transition system models that a model checker generates and high level specification languages such as Statech...
     
Verifying systems with integer constraints and Boolean predicates: a composite approach
Found in: Proceedings of ACM SIGSOFT international symposium on Software testing and analysis (ISSTA '98)
By Christopher League, Richard Gerber, Tevfik Bultan
Issue Date:March 1998
pp. 240
Symbolic mode, checking has proved highly successful for large finite-state systems, in which states can be compactly encoded using binary decision diagrams (BDDs) or their variants. The inherent limitation of this approach is that it cannot be applied to ...
     
Compositional verification by model checking for counter-examples
Found in: Proceedings of the 1996 international symposium on Software testing and analysis (ISSTA '96)
By Jeffrey Fischer, Richard Gerber, Tevfik Bultan
Issue Date:January 1996
pp. 240
Many concurrent systems are required to maintain certain safety and liveness properties. One emerging method of achieving confidence in such systems is to statically verify them using model checking. In this approach an abstract, finite-state model of the ...
     
Composite model-checking: verification with type-specific symbolic representations
Found in: ACM Transactions on Software Engineering and Methodology (TOSEM)
By Christopher League, Richard Gerber, Tevfik Bultan
Issue Date:January 1992
pp. 3-50
There has been a surge of progress in automated verification methods based on state exploration. In areas like hardware design, these technologies are rapidly augmenting key phases of testing and validation. To date, one of the most successful of these met...
     
Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results
Found in: ACM Transactions on Programming Languages and Systems (TOPLAS)
By Richard Gerber, Tevfik Bultan, William Pugh
Issue Date:January 1988
pp. 747-789
Model checking is a powerful technique for analyzing large, finite-state systems. In an infinite state system, however, many basic properties are undecidable. In this article, we present a new symbolic model checker which conservatively evaluates safety a...
     
 1