Search For:

Displaying 1-42 out of 42 total
Runtime Monitoring of Web Service Conversations
Found in: IEEE Transactions on Services Computing
By Jocelyn Simmonds, Yuan Gan, Marsha Chechik, Shiva Nejati, Bill O'Farrell, Elena Litani, Julie Waterhouse
Publication Date: June 2009
pp. 223-244
For a system of distributed processes, correctness can be ensured by (statically) checking whether their composition satisfies properties of interest. However, Web services are distributed processes that dynamically discover properties of other Web service...
 
Matching and Merging of Variant Feature Specifications
Found in: IEEE Transactions on Software Engineering
By Shiva Nejati,Mehrdad Sabetzadeh,Marsha Chechik,Steve Easterbrook,Pamela Zave
Issue Date:November 2012
pp. 1355-1375
Model Management addresses the problem of managing an evolving collection of models by capturing the relationships between models and providing well-defined operators to manipulate them. In this paper, we describe two such operators for manipulating featur...
 
Locating distinguishing features using diff sets
Found in: 2012 27th IEEE/ACM International Conference on Automated Software Engineering (ASE)
By Julia Rubin,Marsha Chechik
Issue Date:September 2012
pp. 242-245
In this paper, we focus on the problem of feature location for families of related software products realized via code cloning. Locating code that corresponds to features in such families is an important task in many software development activities, such a...
 
Managing requirements uncertainty with partial models
Found in: 2012 IEEE 20th International Requirements Engineering Conference (RE)
By Rick Salay,Marsha Chechik,Jennifer Horkoff
Issue Date:September 2012
pp. 1-10
Models are good at expressing information that is known but do not typically have support for representing what information a modeler does not know at a particular phase in the software development process. Partial models address this by being able to prec...
 
Towards a Methodology for Verifying Partial Model Refinements
Found in: Software Testing, Verification, and Validation, 2008 International Conference on
By Rick Salay,Marsha Chechik,Jan Gorzny
Issue Date:April 2012
pp. 938-945
Models are good at expressing information that is known but do not typically have support for representing what information a modeler does not know or does not care about at a particular stage in the software development process. Partial models address thi...
 
Relationship-based change propagation: A case study
Found in: Modeling in Software Engineering, International Workshop on
By Marsha Chechik, Winnie Lai, Shiva Nejati, Jordi Cabot, Zinovy Diskin, Steve Easterbrook, Mehrdad Sabetzadeh, Rick Salay
Issue Date:May 2009
pp. 7-12
Software development is an evolutionary process. Requirements of a system are often incomplete or inconsistent, and hence need to be extended or modified over time. Customers may demand new services or goals that often lead to changes in the design and imp...
 
A relationship-based approach to model management
Found in: Model-Based Methodologies for Pervasive and Embedded Software, International Workshop on
By Marsha Chechik
Issue Date:May 2009
pp. 1
There is a rapidly growing interest in model-based development as a way to increase the level of abstraction and automation in software engineering. The ultimate goal of model-based development is to improve the software process by promoting the use of mod...
 
Synthesis of Partial Behavior Models from Properties and Scenarios
Found in: IEEE Transactions on Software Engineering
By Sebastian Uchitel, Greg Brunet, Marsha Chechik
Issue Date:May 2009
pp. 384-406
Synthesis of behavior models from software development artifacts such as scenario-based descriptions or requirements specifications helps reduce the effort of model construction. However, the models favored by existing synthesis approaches are not sufficie...
 
Global consistency checking of distributed models with TReMer+
Found in: Software Engineering, International Conference on
By Mehrdad Sabetzadeh, Shiva Nejati, Steve Easterbrook, Marsha Chechik
Issue Date:May 2008
pp. 815-818
We present TReMer+, a tool for consistency checking of distributed models (i.e., models developed by distributed teams). TReMer+ works by first constructing a merged model before checking consistency. This enables a flexible way of verifying global consist...
 
Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC
Found in: Formal Methods in Computer Aided Design
By Jocelyn Simmonds, Jessica Davies, Arie Gurfinkel, Marsha Chechik
Issue Date:November 2007
pp. 3-12
When model-checking reports that a property holds on a model, vacuity detection increases user confidence in this result by checking that the property is satisfied in the intended way. While vacuity detection is effective, it is a relatively expensive tech...
 
Consistency Checking of Conceptual Models via Model Merging
Found in: Requirements Engineering, IEEE International Conference on
By Mehrdad Sabetzadeh, Shiva Nejati, Sotirios Liaskos, Steve Easterbrook, Marsha Chechik
Issue Date:October 2007
pp. 221-230
Requirements elicitation involves the construction of large sets of conceptual models. An important step in the analysis of these models is checking their consistency. Existing research largely focuses on checking consistency of individual models and of re...
 
Matching and Merging of Statecharts Specifications
Found in: Software Engineering, International Conference on
By Shiva Nejati, Mehrdad Sabetzadeh, Marsha Chechik, Steve Easterbrook, Pamela Zave
Issue Date:May 2007
pp. 54-64
Model Management addresses the problem of managing an evolving collection of models, by capturing the relationships between models and providing well-defined operators to manipulate them. In this paper, we describe two such operators for manipulating hiera...
 
Behaviour Model Synthesis from Properties and Scenarios
Found in: Software Engineering, International Conference on
By Sebastian Uchitel, Greg Brunet, Marsha Chechik
Issue Date:May 2007
pp. 34-43
Synthesis of behaviour models from software development artifacts such as scenario-based descriptions or requirements specifications not only helps significantly reduce the effort of model construction, but also provides a bridge between approaches geared ...
 
A Relationship-Driven Framework for Model Merging
Found in: Modeling in Software Engineering, International Workshop on
By Mehrdad Sabetzadeh, Shiva Nejati, Steve Easterbrook, Marsha Chechik
Issue Date:May 2007
pp. 2
A key problem in model-based development is merging a set of distributed models into a single seamless model. To merge a set of models, we need to know how they are related. In this position paper, we discuss the methodological aspects of describing the re...
 
Thorough Checking Revisited
Found in: Formal Methods in Computer Aided Design
By Shiva Nejati, Mihaela Gheorghiu, Marsha Chechik
Issue Date:November 2006
pp. 106-116
Recent years have seen a proliferation of 3-valued models for capturing abstractions of systems, since these enable verifying both universal and existential properties. Reasoning about such systems is either inexpensive and imprecise (compositional checkin...
 
Stuttering Abstraction for Model Checkin
Found in: Software Engineering and Formal Methods, IEEE International Conference on
By Shiva Nejati, Arie Gurfinkel, Marsha Chechik
Issue Date:September 2005
pp. 311-320
Abstraction is one of the most effective approaches to improving the applicability and the scalability of modelchecking. The goal of abstraction is to construct a model which is small enough to analyze, yet contains enough detail to allow conclusive analys...
 
Temporal Logic Query Checking: A Tool for Model Exploration
Found in: IEEE Transactions on Software Engineering
By Arie Gurfinkel, Marsha Chechik, Benet Devereux
Issue Date:October 2003
pp. 898-914
<p><b>Abstract</b>—Temporal logic query checking was first introduced by W. Chan in order to speed up design understanding by discovering properties not known a priori. A query is a temporal logic formula containing a special symbol <t...
 
CTL Model-Checking over Logics with Non-Classical Negations
Found in: Multiple-Valued Logic, IEEE International Symposium on
By Marsha Chechik, Wendy MacCaull
Issue Date:May 2003
pp. 293
In earlier work [9], we defined CTL model-checking over finite-valued logics with De Morgan negation. In this paper, we extend this work to logics with intuitionistic, Galois and minimal negations, calling the resulting language \chiCTL. We define \chiCTL ...
 
\chiChek: A Model Checker for Multi-Valued Reasoning
Found in: Software Engineering, International Conference on
By Steve Easterbrook, Marsha Chechik, Benet Devereux, Arie Gurfinkel, Albert Lai, Victor Petrovykh, Anya Tafliovich, Christopher Thompson-Walsh
Issue Date:May 2003
pp. 804
No summary available.
   
Automatic Analysis of Consistency between Requirements and Designs
Found in: IEEE Transactions on Software Engineering
By Marsha Chechik, John Gannon
Issue Date:July 2001
pp. 651-672
<p><b>Abstract</b>—Writing requirements in a formal notation permits automatic assessment of such properties as ambiguity, consistency, and completeness. However, verifying that the properties expressed in requirements are preserved in ot...
 
Model Checking with Multi-Valued Temporal Logics
Found in: Multiple-Valued Logic, IEEE International Symposium on
By Marsha Chechik, Steve Easterbrook, Benet Devereux
Issue Date:May 2001
pp. 0187
Multi-valued logics support the explicit modeling of uncertainty and disagreement by allowing additional truth values in the logic. Such logics can be used for verification of dynamic properties of systems where complete, agreed upon models of the system a...
 
A Framework for Multi-Valued Reasoning over Inconsistent Viewpoints
Found in: Software Engineering, International Conference on
By Steve Easterbrook, Marsha Chechik
Issue Date:May 2001
pp. 0411
Abstract: In requirements elicitation, different stakeholders often hold different views of how a proposed system should behave, resulting in inconsistencies between their descriptions. Consensus may not be needed for every detail, but it can be hard to de...
 
Events in Linear-Time Properties
Found in: Requirements Engineering, IEEE International Conference on
By Dimitrie O. Paun, Marsha Chechik
Issue Date:June 1999
pp. 123
For over a decade, researchers in formal methods tried to create formalisms that permit natural specification of systems and allow mathematical reasoning about their correctness. The availability of fully-automated reasoning tools enables more non-speciali...
 
Symbolic optimization with SMT solvers
Found in: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '14)
By Arie Gurfinkel, Aws Albarghouthi, Marsha Chechik, Yi Li, Zachary Kincaid
Issue Date:January 2014
pp. 607-618
The rise in efficiency of Satisfiability Modulo Theories (SMT) solvers has created numerous uses for them in software verification, program synthesis, functional programming, refinement types, etc. In all of these applications, SMT solvers are used for gen...
     
Managing cloned variants: a framework and experience
Found in: Proceedings of the 17th International Software Product Line Conference (SPLC '13)
By Julia Rubin, Krzysztof Czarnecki, Marsha Chechik
Issue Date:August 2013
pp. 101-110
In our earlier work, we have proposed a generic framework for managing collections of related products realized via cloning -- both in the case when such products are refactored into a single-copy software product line representation and the case when they...
     
Managing forked product variants
Found in: Proceedings of the 16th International Software Product Line Conference - Volume 1 (SPLC '12)
By Andrei Kirshin, Goetz Botterweck, Julia Rubin, Marsha Chechik
Issue Date:September 2012
pp. 156-160
We consider the problem of supporting effective code reuse as part of Software Product Line Engineering. Our approach is based on code forking -- a practice commonly used in industry where new products are created by cloning the existing ones. We propose t...
     
Locating distinguishing features using diff sets
Found in: Proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering (ASE 2012)
By Julia Rubin, Marsha Chechik
Issue Date:September 2012
pp. 242-245
In this paper, we focus on the problem of feature location for families of related software products realized via code cloning. Locating code that corresponds to features in such families is an important task in many software development activities, such a...
     
Weak Alphabet Merging of Partial Behavior Models
Found in: ACM Transactions on Software Engineering and Methodology (TOSEM)
By Dario Fischbein, Greg Brunet, Marsha Chechik, Nicolas D'Ippolito, Sebastian Uchitel
Issue Date:March 2012
pp. 1-47
Constructing comprehensive operational models of intended system behavior is a complex and costly task, which can be mitigated by the construction of partial behavior models, providing early feedback and subsequently elaborating them iteratively. However, ...
     
Robust Vacuity for Branching Temporal Logic
Found in: ACM Transactions on Computational Logic (TOCL)
By Arie Gurfinkel, Marsha Chechik
Issue Date:January 2012
pp. 1-32
There is a growing interest in techniques for detecting whether a logic specification is satisfied too easily, or vacuously. For example, the specification “every request is eventually followed by an acknowledgment” is satisfied vacuously by a ...
     
Partial models: a position paper
Found in: Proceedings of the 8th International Workshop on Model-Driven Engineering, Verification and Validation (MoDeVVa)
By Marsha Chechik, Michalis Famelis, Rick Salay, Shoham Ben-David
Issue Date:October 2011
pp. 1-4
Model-based software development inevitably involves dealing with incomplete information. Yet, MDE methodologies rarely, if ever, address uncertainty in a systematic way. Drawing inspiration from the field of behavioural modeling [6, 4], we propose to use ...
     
Accelerate service integration in your BPM/SOA applications
Found in: Proceedings of the 2010 Conference of the Center for Advanced Studies on Collaborative Research (CASCON '10)
By Allen Chan, Brian Petrini, Marsha Chechik
Issue Date:November 2010
pp. 359-359
Service Integration is the core to enabling any BPM and SOA based applications, and is the mechanism we use to enable new Services from existing applications, or create new Services by composing existing Services.
     
Guided recovery for web service applications
Found in: Proceedings of the eighteenth ACM SIGSOFT international symposium on Foundations of software engineering (FSE '10)
By Jocelyn Simmonds, Marsha Chechik, Shoham Ben-David
Issue Date:November 2010
pp. 247-256
Web service applications are dynamic, highly distributed, and loosely coupled orchestrations of services which are notoriously difficult to debug. In this paper, we describe a user-guided recovery framework for web services. When behavioural correctness pr...
     
RuMoR: monitoring and recovery for BPEL applications
Found in: Proceedings of the IEEE/ACM international conference on Automated software engineering (ASE '10)
By Jocelyn Simmonds, Marsha Chechik
Issue Date:September 2010
pp. 345-346
We describe a RUntime MOnitoring and Recovery framework (RuMoR) for BPEL applications. Our tool checks for behavioral conformance with respect to a set of user-specified properties. When runtime violations are discovered, RuMoR automatically proposes and r...
     
Towards compositional synthesis of evolving systems
Found in: Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering (SIGSOFT '08/FSE-16)
By Marsha Chechik, Mehrdad Sabetzadeh, Pamela Zave, Sebastian Uchitel, Shiva Nejati
Issue Date:November 2008
pp. 1-2
Synthesis of system configurations from a given set of features is an important and very challenging problem. This paper makes a step towards this goal by describing an efficient technique for synthesizing pipeline configurations of feature-based systems. ...
     
Declarative approach for model composition
Found in: Proceedings of the 2008 international workshop on Models in software engineering (MiSE '08)
By Julia Rubin, Marsha Chechik, Steve M. Easterbrook
Issue Date:May 2008
pp. 69-72
Model-based development involves construction, integration, and maintenance of complex models. One of the key problems in model-based development is composing a set of distributed models into a single seamless model. In this paper we propose a declarative ...
     
Behavioural model fusion: an overview of challenges
Found in: Proceedings of the 2008 international workshop on Models in software engineering (MiSE '08)
By Marsha Chechik, Shiva Nejati
Issue Date:May 2008
pp. 69-72
In large-scale model-based development, developers periodically need to combine collections of interrelated models. These models may capture different features of a system, describe alternative perspectives on a single feature, or express ways in which dif...
     
An Eclipse-based tool framework for software model management
Found in: Proceedings of the 2007 OOPSLA workshop on eclipse technology eXchange (eclipse '07)
By Marsha Chechik
Issue Date:October 2007
pp. 55-59
Software development involves the use of many models and Eclipse provides an ideal infrastructure for building tools to support the use of models. While there is a large selection of tools available for working with individual models, there is less support...
     
A manifesto for model merging
Found in: Proceedings of the 2006 international workshop on Global integrated model management (GaMMa '06)
By Greg Brunet, Marsha Chechik, Mehrdad Sabetzadeh, Nan Niu, Shiva Nejati, Steve Easterbrook
Issue Date:May 2006
pp. 5-12
If a modeling task is distributed, it will frequently be necessary to merge models developed by different team members. Existing approaches to model merging make assumptions about the types of model to be merged, and the nature of the relationship between ...
     
Let's agree to disagree
Found in: Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering (ASE '05)
By Marsha Chechik, Shiva Nejati
Issue Date:November 2005
pp. 287-290
Almost every kind of software development periodically needs to merge models. Perhaps they come from different stakeholders during the requirements analysis phase, or perhaps they are modifications of the same model done independently by several groups of ...
     
Merging partial behavioural models
Found in: Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering (SIGSOFT '04/FSE-12)
By Marsha Chechik, Sebastian Uchitel
Issue Date:October 2004
pp. 253-265
Constructing comprehensive operational models of intended system behaviour is a complex and costly task. Consequently, practitioners have adopted techniques that support incremental elaboration of partial behaviour descriptions. A noteworthy example is the...
     
Model exploration with temporal logic query checking
Found in: Proceedings of the tenth ACM SIGSOFT symposium on Foundations of software engineering (SIGSOFT '02/FSE 10)
By Arie Gurfinkel, Benet Devereux, Marsha Chechik
Issue Date:November 2002
pp. 139-148
A temporal logic query is a temporal logic formula with placeholders. Given a model, a solution to a query is a set of assignments of propositional formulas to placeholders, such that replacing the placeholders with any of these assignments results in a te...
     
Automatic verification of requirements implementation
Found in: Proceedings of the 1994 international symposium on Software testing and analysis (ISSTA '94)
By John Gannon, Marsha Chechik
Issue Date:August 1994
pp. 1-14
Requirements of event-based systems can be automatically analyzed to determine if certain safety properties hold. However, we lack comparable methods to verify that implementations maintain the properties guaranteed by the requirements. We have built a too...
     
 1