Bibliography
@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob tmpbib.bib -c 'key : "PeerReview"' bib.bib}}
@inproceedings{BH10iscram,
key = {PeerReview},
author = {Bjurling B. and Hansen P.},
title = {{Contracts for Information Sharing in Collaborative Networks}},
booktitle = {7th International ISCRAM Conference},
optpages = {},
year = {2010},
opteditor = {},
optvolume = {},
address = {Seattle, USA},
month = {May},
optpublisher = {IEEE},
pdf = {publications/BH10iscram.pdf},
optabstract = {In a web service composition, an electronic contract (e-contract) regulates how the services participating in the composition should behave, including the restrictions that these services must fulfill, such as real-time constraints. In this work we present a visual model that allows us to specify e-contracts in a user friendly way, including conditional behavior and realtime constraints. A case study is presented to illustrate how this visual model defines e-contracts and a preliminary evaluation of the model is also done.}
}
@inproceedings{ChenHHKLLLNORSYZ07,
key = {PeerReview},
author = {Zhenbang Chen and
Abdel Hakim Hannousse and
Dang Van Hung and
Istvan Knoll and
Xiaoshan Li and
Zhiming Liu and
Yang Liu and
Qu Nan and
Joseph C. Okika and
Anders P. Ravn and
Volker Stolz and
Lu Yang and
Naijun Zhan},
title = {Modelling with Relational Calculus of Object and Component
Systems - rCOS},
editor = {Andreas Rausch and
Ralf Reussner and
Raffaela Mirandola and
Frantisek Plasil},
booktitle = {The Common Component Modeling Example: Comparing Software
Component Models -- result from the Dagstuhl research seminar
for CoCoME},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5153},
year = {2008},
isbn = {978-3-540-85288-9},
pages = {116-145},
doi = {10.1007/978-3-540-85289-6_6}
}
@proceedings{OS09flacos,
key = {PeerReview},
title = {{Special Issue: Formal Languages and Analysis of Contract-Oriented Software (FLACOS'07)}},
year = {2009},
editor = {Olaf Owe and Gerardo Schneider},
volume = {78},
number = {5},
series = {{The Journal of Logic and Algebraic Programming}},
optaddress = {},
month = {May},
optorganization = {},
issn = {1567-8326},
isbn = {},
publisher = {Elsevier}
}
@inproceedings{MCD+,
key = {PeerReview},
author = {Enrique Martinez and Emilia Cambronero and Gregorio Diaz and Gerardo Schneider},
title = {{A Model for Visual Specification of e-Contracts}},
booktitle = {The 7th International Conference on Services Computing (SCC'10)},
optpages = {},
year = {2010},
opteditor = {},
optvolume = {},
address = {Miami, USA},
month = {July},
publisher = {IEEE},
issn = {},
isbn = {},
pdf = {http://folk.uio.no/gerardo/scc2010.pdf},
note = {To appear},
abstract = {In a web service composition, an electronic contract (e-contract) regulates how the services participating in the composition should behave, including the restrictions that these services must fulfill, such as real-time constraints. In this work we present a visual model that allows us to specify e-contracts in a user friendly way, including conditional behavior and realtime constraints. A case study is presented to illustrate how this visual model defines e-contracts and a preliminary evaluation of the model is also done.}
}
@inproceedings{FPS09atva,
key = {PeerReview},
author = {Stephen Fenech and
Gordon J. Pace and
Gerardo Schneider},
title = {CLAN: A Tool for Contract Analysis and Conflict Discovery},
booktitle = {7th
International Symposium on Automated Technology for Verification and Analysis (ATVA'09)},
year = {2009},
pages = {90-96},
editor = {Zhiming Liu and
Anders P. Ravn},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5799},
isbn = {978-3-642-04760-2},
month = {October},
address = {Macao, China},
pdf = {http://folk.uio.no/gerardo/atva09.pdf},
opturl = {publications/slides/wollic09slides.pdf.gz},
abstract = {As Service-Oriented Architectures are more widely adopted, it becomes more important to adopt measures for ensuring that the services satisfy functional and non-functional requirements. One approach is the use of contracts based on deontic logics, expressing obligations, permissions and prohibitions of the different actors. The use of explicit contracts enables various analysis techniques to be used when using services. A challenging aspect is that of service composition, in which the contracts composed together may result in conflicting situations. Especially in a context where services may be dynamically composed, the need for automated techniques to analyse contracts and ensure their soundness are crucial. In this paper, we present CLAN, a tool for automatic analysis of conflicting clauses of contracts written in the contract language CL. We present a small case study of an airline check-in desk illustrating the use of the tool.},
optkeywords = {e-contracts, legal contracts, deontic logic, PDL, synchrony, semantics, normative structure, decidability},
doi = {10.1007/978-3-642-04761-9_8}
}
@inproceedings{FPS09ictac,
key = {PeerReview},
author = {Stephen Fenech and
Gordon J. Pace and
Gerardo Schneider},
title = {Automatic Conflict Detection on Contracts},
booktitle = {6th International Colloquium on Theoretical Aspects of Computing (ICTAC'09)},
editor = {Martin Leucker and
Carroll Morgan},
publisher = {Springer},
year = {2009},
pages = {200-214},
month = {August},
address = {Kuala Lumpur, Malaysia},
series = {Lecture Notes in Computer Science},
isbn = {978-3-642-03465-7},
volume = 5684,
pdf = {http://folk.uio.no/gerardo/ictac09-contracts.pdf},
opturl = {publications/slides/wollic09slides.pdf.gz},
abstract = {Industry is currently pushing towards Service-Oriented Architectures, where code execution is not limited to the organisational borders but may be extended beyond, to sources typically not accessible. Contracts, expressing obligations, permissions and prohibitions of the different actors, can be used to protect the interests of the organisations engaged in such service exchange. The, potentially dynamic, composition of different services with different contracts, and the combination of service contracts with local contracts can give rise to unexpected conflicts, exposing the need for automatic techniques for contract analysis. In this paper we look at automatic analysis techniques for contracts written in the contract language CL. We present a trace semantics of CL suitable for conflict analysis, and a decision procedure for detecting conflicts (together with its proof of soundness, completeness and termination). We also discuss its implementation and look into the applications of the contract analysis approach we present. These techniques are applied to a small case study of an airline check-in desk.},
optkeywords = {e-contracts, legal contracts, deontic logic, PDL, synchrony, semantics, normative structure, decidability},
doi = {10.1007/978-3-642-03466-4_13}
}
@inproceedings{P10concur,
key = {PeerReview},
title = {{Modal Logic over Higher Dimensional Automata}},
author = {Cristian Prisacariu},
booktitle = {21st International Conference on Concurrency Theory (CONCUR10)},
editor = {Paul Gastin and Francois Laroussinie},
publisher = {Springer},
optpages = {335-349},
year = 2010,
month = {August},
address = {Paris, France},
series = {Lecture Notes in Computer Science},
optisbn = {978-3-642-02260-9},
optvolume = 5514,
pdf = {publications/concur10.pdf},
ps = {publications/concur10.ps},
dvi = {publications/concur10.dvi},
opturl = {publications/slides/concur10slides.pdf.gz},
abstract = {Higher dimensional automata (HDA) are a model of concurrency that can express most of the traditional partial order models like Mazurkiewicz traces, pomsets, event structures, or Petri nets. Modal logics, interpreted over Kripke structures, are the logics for reasoning about sequential behavior and interleaved concurrency. Modal logic is a well behaved subset of first-order logic; many variants of modal logic are decidable. However, there are no modal-like logics for the more expressive HDA models. In this paper we introduce and investigate a modal logic over HDAs which incorporates two modalities for reasoning about 'during' and 'after'. We prove that this general higher dimensional modal logic (HDML) is decidable and we define a complete axiomatic system for it. We also show how, when the HDA model is restricted to Kripke structures, a syntactic restriction of HDML becomes the standard modal logic. Then we isolate the class of HDAs that encode Mazurkiewicz traces and show how HDML can be restricted to LTrL (the linear time temporal logic over Mazurkiewicz traces).},
keywords = {higher dimensional automata, Mazurkiewicz trace theory, event structures, linear temporal logic, LTrL, modal logic, 'during' modality, axiomatization completeness and decidability, filtration},
optdoi = {10.1007/978-3-642-02261-6_27}
}
@article{pri09jlap_SKA,
key = {PeerReview},
title = {{Synchronous Kleene Algebra}},
author = {Cristian Prisacariu},
journal = {The Journal of Logic and Algebraic Programming (JLAP)},
optvolume = {},
optnumber = {},
year = {2009},
optpages = {321-328},
opteditor = {},
optpublisher = {Elsevier},
month = {December},
optisbn = {},
optissn = {},
note = {(accepted)},
pdf = {publications/jlap09.pdf},
ps = {publications/jlap09.ps},
abstract = {The work presented here investigates the combination of Kleene algebra with the synchrony model of concurrency from Milner's SCCS calculus. The resulting algebraic structure is called synchronous Kleene algebra. Models are given in terms of sets of synchronous strings and finite automata accepting synchronous strings. The extension of synchronous Kleene algebra with Boolean tests is presented together with models on sets of guarded synchronous strings and the associated automata on guarded synchronous strings. Completeness w.r.t. the standard interpretations is given for each of the two new formalisms. Decidability follows from completeness. Kleene algebra with synchrony should be included in the class of true concurrency models. In this direction, a comparison with Mazurkiewicz traces is made which yields their incomparability with synchronous Kleene algebras (one cannot simulate the other). On the other hand, we isolate a class of pomsets which captures exactly synchronous Kleene algebras. We present an application to Hoare-like reasoning about parallel programs in the style of synchrony.},
keywords = {Universal algebra, Kleene algebra, Boolean tests, synchrony, SCCS calculus, concurrency models, automata theory, completeness, Hoare logic},
optdoi = {}
}
@inproceedings{PS09wollic,
key = {PeerReview},
title = {{CL: An Action-based Logic for Reasoning about Contracts}},
author = {Cristian Prisacariu and Gerardo Schneider},
booktitle = {16th Workshop on Logic, Language, Information and Computation (WOLLIC09)},
editor = {Makoto Kanazawa and Hiroakira Ono and Ruy de Queiroz},
publisher = {Springer},
pages = {335-349},
year = 2009,
month = {June},
address = {Tokyo, Japan},
series = {Lecture Notes in Computer Science},
isbn = {978-3-642-02260-9},
volume = 5514,
pdf = {publications/wollic09.pdf},
ps = {publications/wollic09.ps},
dvi = {publications/wollic09.dvi},
opturl = {publications/slides/wollic09slides.pdf.gz},
abstract = {This paper presents a new version of the CL contract specification language. CL combines deontic logic with propositional dynamic logic but it applies the modalities exclusively over structured actions. CL features synchronous actions, conflict relation, and an action negation operation. The CL version that we present here is more expressive and has a cleaner semantics than its predecessor. We give a direct semantics for CL in terms of normative structures. We show that CL respects several desired properties from legal contracts and is decidable. We relate this semantics with a trace semantics of CL which we used for run-time monitoring contracts.},
keywords = {e-contracts, legal contracts, deontic logic, PDL, synchrony, semantics, normative structure, decidability},
doi = {10.1007/978-3-642-02261-6_27}
}
@inproceedings{PS08atva,
key = {PeerReview},
title = {Run-time {M}onitoring of {E}lectronic {C}ontracts},
author = {Marcel Kyas and Cristian Prisacariu and Gerardo Schneider},
booktitle = {6th International Symposium on Automated Technology for Verification and Analysis (ATVA08)},
editor = {Moonzoo Kim and Mahesh Viswanathan},
publisher = {Springer},
pages = {397-407},
year = {2008},
month = {October},
address = {Seoul, South-Korea},
series = {Lecture Notes in Computer Science},
volume = 5311,
pdf = {publications/atva08.pdf},
abstract = {Electronic inter-organizational relationships are governed by contracts regulating their interaction. It is necessary to run-time monitor the contracts, as to guarantee their fulfillment as well as the enforcement of penalties in case of violations. The present work shows how to obtain a run-time monitor for contracts written in CL, a formal specification language which allows to write conditional obligations, permissions and prohibitions over actions. We first give a trace semantics for CL which formalizes the notion of a trace fulfills a contract. We show how to obtain, for a given contract, an alternating Buchi automaton which accepts exactly the traces that fulfill the contract. This automaton is the basis for obtaining a finite state machine which acts as a run-time monitor for CL contracts.},
keywords = {alternating Buchi automata, electronic contracts, trace semantics, deontic logic, modal logic},
doi = {10.1007/978-3-540-88387-6_34}
}
@inproceedings{PS08csf,
key = {PeerReview},
author = {Gordon J. Pace and Gerardo Schneider},
title = {Challenges in the Specification of Full Contracts},
booktitle = {{Integrated Formal Methods (iFM'09)}},
optpages = {},
optvolume = {},
series = {LNCS},
address = {D\"useldorf, Germany},
year = {2009},
month = {February},
note = {To appear.},
pdf = {publications/ifm2009.pdf},
abstract = {The complete specification of full contracts ---contracts which
include tolerated exceptions, and which enable reasoning about the
contracts themselves, can be achieved using a combination of temporal
and deontic concepts. In this paper we discuss the challenges in
combining deontic and other relevant logics, in particular focusing on
operators for choice, obligations over sequences, contrary-to-duty
obligations, and how internal and external decisions may be
incorporated in an action-based language for specifying contracts. We
provide different viable interpretations and approaches for the
development of such a sound logic and outline challenges for the
future.}
}
@inproceedings{FOP+08bsc,
key = {PeerReview},
author = {Stephen Fenech and Joseph Okika and Gordon J. Pace and Anders P. Ravn and Gerardo Schneider},
title = {On the Specification of Full Contracts},
booktitle = {6th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA'09)},
optpages = {},
series = {ENTCS},
address = {York, UK},
year = {2009},
month = {March},
note = {To appear},
abstract = {Contracts are specifications of properties of an interface to a software component; in this paper we focus on behavioural properties.
We consider the problem of giving a full contract that specifies not only the normal behaviour, but also special cases and tolerated exceptions.
We conjecture that operational specifications are well suited for normal cases, but are less easily extended for exceptional cases.
Logic based specifications are essentially compositional, helping in some cases the specification of exceptional cases.
This hypothesis is investigated by comparing specifications in CSP (operational) with specifications in LTL, CTL and a deontic logic based language CL. The specifications give successive extensions to a contract for a Cash Desk example.
The outcome of the experiment supports
the conjecture and demonstrates clear differences in the basic descriptive power of the formalisms.},
pdf = {publications/fesca09-cocome.pdf}
}
@inproceedings{OS08wos,
key = {PeerReview},
author = {Olaf Owe and Gerardo Schneider},
title = {Wrap your Objects Safely},
booktitle = {6th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA'09)},
optpages = {},
series = {ENTCS},
address = {York, UK},
year = {2009},
month = {March},
note = {To appear},
abstract = {Despite the effort of researchers on distributed systems, programming languages, and security, there is still no good solution offering basic constructs for guaranteeing minimal security at the programming language level. In particular, the notion of a wrapper around an object controlling its interaction with the environment has not properly been addressed at the programming language level. This kind of ``local firewall'' may play two different roles: (1) The untrusted part is the object inside the wrapper; (2) The untrusted part is the environment. In this paper we propose the addition of a language primitive for creating wrapped objects, and sketch a formalization based on a minimal object-oriented language for distributed systems, based on asynchronous communication.},
pdf = {publications/fesca09-wrappers.pdf}
}
@inproceedings{CLSYR07,
key = {PeerReview},
author = {Zhenbang Chen and Zhiming Liu and Volker Stolz and Lu Yang and Anders P. Ravn},
title = {A refinement driven component-based design},
booktitle = {Proceedings of the 12th IEEE International Conference on Engineering Complex Computer Systems (ICECCS07)},
month = {July},
year = {2007},
isbn = {0-7695-2895-3},
pages = {277-289},
publisher = {IEEE Computer Society},
address = {Auckland, New Zealand},
abstract = {Modern software applications ranging from enterprise to embedded systems are becoming increasingly complex, and require very high levels of dependability assurance. The most effective means to handle complexity is separation of concerns and incremental development, and assurance of dependability requires formal methods. We report here our experience on these issues in an application of a formal calculus, rCOS, to a component-based design of the point of sale system (POS). We demonstrate the possibility in scaling-up correctness by design and discuss how rCOS may be integrated with current and emerging software engineering tools.},
pdf = {publications/iceccs07.pdf},
keywords = {Software development process, object-orientation, component-based modeling, refinement}
}
@inproceedings{DKP06snvo,
key = {PeerReview},
author = {Sakyibea Darko-Ampem and Maria Katsoufi and Pablo Giambiagi},
title = {{Secure Negotiation in Virtual Organizations}},
booktitle = {Advances in Quality of Service Management (AQuSerM 2006),
EDOCW'06},
pages = {48--55},
year = {2006},
address = {Hong Kong, China},
month = {October},
publisher = {IEEE Computer Society},
optpdf = {publications/AQuSerM06.pdf},
optabstract = {}
}
@inproceedings{HS07,
key = {PeerReview},
author = {Hammer, Johs H. and Schneider, Gerardo},
title = {On the definition and policies of confidentiality},
booktitle = {Third International Symposium on Information Assurance and Security (IAS'07).},
pages = {337--342},
address = {Manchester, UK},
month = {August},
publisher = {IEEE Computer Society},
year = 2007,
isbn = {ISBN 978-0-7695-2876-2},
pdf = {publications/ias2007.pdf},
abstract = {In this paper we propose a more general definition of confidentiality, as an aspect of information security including information flow control. We discuss central aspects of confidentiality and their relation with norms and policies, and we introduce a language, with a deontic flavor, to express such norms and policies.
Our language may be regarded as a first step towards a formal specification of security policies for confidentiality.
We provide a number of examples of useful norms on confidentiality, and we discuss confidentiality policies from real scenarios.}
}
@inproceedings{NIK07,
key = {PeerReview},
author = {Arild Torjusen and Olaf Owe and Gerardo Schneider},
title = {Towards integration of {XML} in the {C}reol object-oriented language},
booktitle = {Proceedings of {Norsk Informatikkonferanse 2007} (NIK'07)},
year = 2007,
pages = {107--111},
address = {Oslo, Norway},
month = {November},
editor = {Frode Eika Sandnes},
publisher = {Tapir Akademisk Forlag},
isbn = {978-82-519-2272-2},
pdf = {publications/nik07.pdf},
abstract = {The integration of XML documents in object-oriented programming languages is becoming paramount with the advent of the use of Internet in new applications like web services. Such an integration is not easy in general and demands a careful language design. In this paper we propose an extension to Creol, a high level object-oriented modeling language for distributed systems, for handling XML documents.}
}
@inproceedings{COR07web,
key = {PeerReview},
author = {Emilia Cambronero and Joseph C. Okika and Anders P. Ravn},
title = {Analyzing {W}eb {S}ervice {C}ontracts - {A}n {A}spect {O}riented {A}pproach.},
booktitle = {Proceedings of the International Conference on Mobile Ubiquitous Computing, Systems, Services and Technologies (UBICOMM'2007)},
month = {November},
year = {2007},
isbn-10 = {0-7695-2993-3},
pages = {149 - 154},
address = {Papeete, French Polynesia (Tahiti)},
publisher = {IEEE Computer Society Press},
pdf = {publications/cambronero.okika.ravn-AnalyzingWebServiceContracts.pdf},
abstract = {Web services should be dependable, because businesses rely on them. For that purpose the Service Oriented Architecture has standardized specifications at a syntactical level. In this paper, we demonstrate how such specifications are used to derive semantic models in the form of (timed) automata. These can be used to model check functional and behavioural properties of a given service. Since there might be several specifications dealing with different aspects, one must also check that these automata are consistent, where we propose to set up a suitable simulation relation. The proposed techniques are illustrated with a small case study.},
optannote = {}
}
@inproceedings{OSS07coc,
key = {PeerReview},
author = {Olaf Owe and Gerardo Schneider and Martin Steffen},
title = {Components, {O}bjects, and {C}ontracts},
booktitle = {{6th Workshop on Specification And Verification of Component-Based Systems (SAVCBS'07)}},
optcrossref = {},
optkey = {},
pages = {91--94},
year = {2007},
opteditor = {},
optvolume = {},
optnumber = {},
series = {ACM Digital Library},
address = {Dubrovnik, Croatia},
month = {September},
optorganization = {},
optpublisher = {},
pdf = {publications/savcbs2007.pdf},
abstract = {Being a composite part of a larger system, a crucial feature of a component is its interface, as it describes the component's interaction with the rest of the system in an abstract manner. It is now commonly accepted that simple, functional interfaces are not expressive enough for components, and the trend is towards behavioral interfaces. We propose to go a step further and enhance components with contracts, i.e., agreements between two or more components on what they are obliged, permitted and forbidden when interacting. This way, contracts are modelled after legal contracts from conventional business or judicial arenas. Indeed, our work aims at a framework for e-contracts, i.e., ''electronic'' versions of legal documents describing the parties' respective duties. We take the object-oriented, concurrent programming language Creol as starting point and extend it with a notion of components. We then discuss a framework where components are accompanied by contracts and we sketch some ideas on how analysis of compatibility and compositionality could be done in such a setting.},
optannote = {}
}
@inproceedings{PPS07mcc,
key = {PeerReview},
author = {Gordon Pace and Cristian Prisacariu and Gerardo Schneider},
title = {Model {C}hecking {C}ontracts --A Case Study},
booktitle = {{5th International Symposium on Automated Technology for Verification and Analysis (ATVA'07)}},
pages = {82--97},
year = {2007},
volume = {4762},
series = {Lecture {N}otes in {C}omputer {S}cience},
address = {Tokyo, Japan},
month = {October},
publisher = {Springer},
pdf = {publications/atva2007.pdf},
abstract = {Contracts are agreements between distinct parties that determine rights and obligations on their signatories, and have been introduced in order to reduce risks and to regulate inter-business relationships. In this paper we show how a conventional contract can be written in the contract language CL, how to model the contract, and finally how to verify properties of the model using the NuSMV model checking tool.}
}
@inproceedings{PS07fle,
key = {PeerReview},
title = {A {F}ormal {L}anguage for {E}lectronic {C}ontracts},
author = {Prisacariu, Cristian and Schneider, Gerardo},
booktitle = {9th IFIP International Conference on
Formal Methods for Open Object-Based Distributed Systems (FMOODS'07)},
editor = {Bonsangue, Marcello and Johnsen, Einar Broch},
address = {Paphos, Cyprus},
publisher = {Springer},
pages = {174-189},
year = 2007,
month = {June},
series = {Lecture Notes in Computer Science},
volume = 4468,
abstract = {In this paper we propose a formal language for writing electronic contracts, based on the deontic notions of obligation, permission, and prohibition. We
take an ought-to-do approach, where deontic operators are applied to actions instead of state-of-affairs. We propose an extension of the mu-calculus in order to
capture the intuitive meaning of the deontic notions, and to express deterministic and concurrent actions. We provide a translation of the contract language into the
logic, the semantics of which faithfully captures the meaning of obligation, permission and prohibition. We also show how our language captures most of the intuitive
desirable properties of electronic contracts, as well as how it avoids most of the classical paradoxes of deontic logic. We finally show its applicability on a
contract example.},
keywords = {mu-calculus, e-contracts, specification language, concurrency},
pdf = {publications/fmoods2007.pdf}
}
@inproceedings{GOSR06lbs,
key = {PeerReview},
title = {Language-{B}ased {S}upport for {S}ervice {O}riented {A}rchitectures: {F}uture {D}irections},
author = {Giambiagi, Pablo and Owe, Olaf and Ravn, Anders P. and Schneider, Gerardo},
booktitle = {ICSOFT (1)},
editor = {Filipe, Joaquim and Shishkov, Boris and Helfert, Markus},
publisher = {INSTICC Press},
address = {Set\'ubal, Portugal},
pages = {339--344},
year = 2006,
isbn = {972-8865-69-4},
month = {September},
abstract = {The fast evolution of the Internet has popularized service-oriented architectures (SOA) with their promise of dynamic IT-supported inter-business collaborations. Yet this popularity does not reflect on the number of actual applications using the architecture. Programming models in use today make a poor match for the distributed, loosely-coupled, document-based nature of SOA. The gap is actually increasing. For example, interoperability between different organizations, requires contracts to reduce risks. Thus, high-level models of contracts are making their way into service-oriented architectures, but application developers are still left to their own devices when it comes to writing code that will comply with a contract. This paper surveys existing and future directions regarding language-based solutions to the above problem.},
keywords = {},
pdf = {publications/icsoft2006.pdf}
}
@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob tmpbib.bib -c 'key : "TechRep" or key : "other"' bib.bib}}
@techreport{prisacariu10TR393,
key = {TechRep},
title = {{Modal Logic over Higher Dimensional Automata - technicalities}},
author = {Prisacariu, Cristian},
publisher = {Department of Informatics, University of Oslo},
address = {Norway},
pages = {42},
year = 2010,
isbn = {82-7368-354-0},
month = {January},
number = 393,
institution = {Department of Informatics, University of Oslo},
issn = {0806-3036},
abstract = {Higher dimensional automata (HDAs) are a model of concurrency that can express most of the traditional partial order models like Mazurkiewicz traces, pomsets, event structures, or Petri nets. Modal logics, interpreted over Kripke structures, are the logics for reasoning about sequential behavior and interleaved concurrency. Modal logic is a well behaved subset of first-order logic; many variants of modal logic are decidable. However, there are no modal-like logics for the more expressive HDAs models. In this paper we introduce and investigate a modal logic over HDAs. We prove that this general higher dimensional modal logic (HDML) is decidable and we define a complete axiomatic system for it. We also show how, when the HDA model is restricted to Kripke structures, a syntactic restriction of HDML becomes the standard modal logic. Then we isolate the class of HDAs that encode Mazurkiewicz traces and show how HDML can be restricted to the LTrL logic over Mazurkiewicz traces.},
keywords = {higher dimensional automata, Mazurkiewicz trace theory, event structures, linear temporal logic for traces, LTrL, axiomatization completeness, decidability},
pdf = {publications/TR393.pdf},
ps = {publications/TR393.ps}
}
@techreport{PS08flacos,
key = {TechRep},
author = {Gordon J. Pace and Gerardo Schneider},
title = {{FLACOS'08 Workshop Proceedings}},
institution = {Department of Informatics, University of Oslo},
year = {2008},
number = {377},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
optisbn = {82-7368-337-0},
optissn = {0806-3036},
month = {October},
note = {Editors},
pdf = {publications/report-UiO-377.pdf}
}
@techreport{prisacariu08TRdeontic,
key = {TechRep},
title = {Deontic Modalities over Synchronous Actions - Technicalities},
author = {Prisacariu, Cristian},
publisher = {Dept. Informatics, Univ. Oslo},
address = {Norway},
pages = {52},
year = 2008,
isbn = {82-73-68341-9},
month = {December},
number = 381,
institution = {Dept. Informatics, Univ. Oslo},
issn = {0806-3036},
abstract = {The work reported here steams from the need of a more practical interpretation of the deontic logic. We follow the recent ought-to-do approach where the deontic modalities are applied over actions instead of over expressions. This allows an easy integration with the propositional dynamic logic or the modal mu-calculus; and from here a whole set of tools e.g. for model checking or for runtime monitoring can now be easily adapted to the deontic modalities. We consider the regular actions enriched with the synchrony operator to model synchronous execution of actions. The interpretation that we give to the logic is biased by the natural properties which the deontic modalities are required to respect when used in the legal environment. Technically the paper presents a semantics based on an algebraic formalism for the actions and on normative structures for the deontic modalities. One source of difficulty comes from the synchrony operator over actions. The properties of the deontic modalities are presented as validities or nonvalidities. The logic enjoys the tree model property and the finite model property and decidability follows from this.},
keywords = {Deontic logic of actions, synchronous actions, tree model, normative structure, legal contracts},
pdf = {publications/TR381.pdf}
}
@techreport{Pri08tr1,
key = {TechRep},
title = {Extending {K}leene {A}lgebra with {S}ynchrony - technicalities},
author = {Prisacariu, Cristian},
publisher = {Department of Informatics, University of Oslo},
address = {Oslo, Norway},
pages = {56},
number = {376},
year = 2008,
month = {October},
isbn = {82-7368-336-2},
issn = {0806-3036},
abstract = {The work reported here investigates the introduction of synchrony into Kleene algebra. The resulting algebraic structure is called synchronous Kleene algebra. Models are given in terms of regular sets of concurrent strings and finite automata accepting concurrent strings. The extension of synchronous Kleene algebra with Boolean tests is presented together with models on regular sets of guarded concurrent strings and the associated automata on guarded concurrent strings. Completeness w.r.t. the standard interpretations is given in each case. Decidability follows from completeness. A comparison with Mazurkiewicz traces is made which yields their incomparability with the synchronous Kleene algebra (one cannot simulate the other). Applications to respectively deontic logic of actions and to propositional dynamic logic with synchrony are sketched.},
institution = {Department of Informatics, University of Oslo},
keywords = {Kleene algebra, synchronous CCS, guarded strings, finite state automata, completeness},
pdf = {publications/TR376.pdf}
}
@techreport{PS08tr2,
key = {TechRep},
title = {Run-time {M}onitoring of {E}lectronic {C}ontracts - theoretical results},
author = {Kyas, Marcel and Prisacariu, Cristian and Schneider, Gerardo},
publisher = {Department of Informatics, University of Oslo},
address = {Oslo, Norway},
pages = {64},
number = {378},
year = 2008,
month = {November},
isbn = {82-7368-338-9},
issn = {0806-3036},
abstract = {This technical report is an extension of the paper published in the conference ATVA 2008, and includes more motivation, complete examples, and complete proofs for all results presented in ATVA 2008, as well as other additional results. Electronic inter-organizational relationships are governed by contracts regulating their interaction. It is necessary to run-time monitor the contracts, as to guarantee their fulfillment as well as the enforcement of penalties in case of violations. The present work shows how to obtain a run-time monitor for contracts written in CL, a formal specification language which allows to write conditional obligations, permissions and prohibitions over actions. We first give a trace semantics for CL which formalizes the notion of a trace fulfills a contract. We show how to obtain, for a given contract, an alternating Buchi automaton which accepts exactly the traces that fulfill the contract. This automaton is the basis for obtaining a finite state machine which acts as a run-time monitor for CL contracts.},
institution = {Department of Informatics, University of Oslo},
keywords = {Electronic contracts, Kleene algebra, guarded rooted trees, concurrency, completeness},
pdf = {publications/TR378.pdf}
}
@techreport{PS08tr3,
key = {TechRep},
title = {CL -- A Logic for Reasoning about Legal Contracts: -- Semantics},
author = {Prisacariu, Cristian and Schneider, Gerardo},
publisher = {Department of Informatics, University of Oslo},
address = {Oslo, Norway},
pages = {80},
year = 2008,
month = {February},
number = 371,
isbn = {82-7368-330-3},
issn = {0806-3036},
abstract = {},
institution = {Department of Informatics, University of Oslo},
keywords = {Electronic contracts, Kripke semantics, trace semantics, deontic logic, concurrency},
pdf = {publications/TR371.pdf}
}
@techreport{JOS07nf,
key = {TechRep},
author = {Einar B. Johnsen and Olaf Owe and Gerardo Schneider},
editor = {Einar B. Johnsen and Olaf Owe and Gerardo Schneider},
title = {{NWPT'07/FLACOS'07 {W}orkshop {P}roceedings}},
institution = {Department of Informatics, University of Oslo},
year = {2007},
number = {366},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
optisbn = {82-7368-324-9},
optissn = {0806-3036},
month = {October},
note = {Editors},
pdf = {publications/TR366.pdf},
optabstract = {}
}
@techreport{PPS07TRmcc,
key = {TechRep},
author = {Gordon Pace and Cristian Prisacariu and Gerardo Schneider},
title = {Model {C}hecking {C}ontracts --A Case Study},
institution = {Department of Informatics, University of Oslo},
year = {2007},
number = {362},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
optisbn = {82-7368-320-6},
optissn = {0806-3036},
month = {October},
pdf = {publications/TR362.pdf},
abstract = {Contracts are agreements between distinct parties that determine rights and obligations on their signatories, and have been introduced in order to reduce risks and to regulate inter-business relationships. In this paper we show how a conventional contract can be written in the contract language CL, how to model the contract, and finally how to verify properties of the model using the NuSMV model checking tool.}
}
@techreport{OSS07,
key = {TechRep},
author = {Olaf Owe and Gerardo Schneider and Martin Steffen},
title = {Components, {O}bjects, and {C}ontracts},
institution = {Department of Informatics, University of Oslo},
year = {2007},
number = {363},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
optisbn = {82-7368-321-4},
optissn = {0806-3036},
month = {August},
pdf = {publications/TR363.pdf},
abstract = {Being a composite part of a larger system, a crucial feature of a component is its \emph{interface}, as it describes the component's interaction with the rest of the system in an abstract manner. It is now commonly accepted that simple, functional interfaces are not expressive enough for components, and the trend is towards \emph{behavioral} interfaces. We propose to go a step further and enhance components with \emph{contracts}, i.e., agreements between two or more components on what they are \emph{obliged,} \emph{permitted} and \emph{forbidden} when interacting. This way, contracts are modelled after legal contracts from conventional business or judicial arenas. Indeed, our work aims at a framework for \emph{e-contracts}, i.e., ''electronic'' versions of legal documents describing the parties' respective duties. We take the object-oriented, concurrent programming language \emph{Creol} as starting point and extend it with a notion of components. We then discuss a framework where components are accompanied by contracts and we sketch some ideas on how analysis of compatibility and compositionality could be done in such a setting.}
}
@techreport{PS07tr361,
key = {TechRep},
title = {An {A}lgebraic {S}tructure for the {A}ction-{B}ased {C}ontract {L}anguage {CL} - theoretical results},
author = {Prisacariu, Cristian and Schneider, Gerardo},
publisher = {Department of Informatics, University of Oslo},
address = {Oslo, Norway},
pages = {64},
number = {361},
year = 2007,
month = {July},
abstract = {We introduce in this paper an algebra of actions specially tailored to serve as basis of an action-based formalism for writing electronic contracts. The proposed algebra is based on the work on Kleene algebras but does not consider the Kleene star and introduces a new constructor for modelling concurrent actions. The algebraic structure is resource-aware and incorporates special actions called tests. In order to be in accordance with the intuition behind electronic contracts we consider new properties of the algebraic structure, in particular a conflict relation and a demanding partial order. We also study a canonical form of the actions which, among other things, helps to naturally define a notion of action negation. Our action negation is more general than just negation of atomic actions, but more restricted than the negation involving the universal relation. A standard interpretation of the algebra is given in terms of guarded rooted trees with specially defined operations on them. The algebra is proven to be complete over the standard interpretation.},
institution = {Department of Informatics, University of Oslo},
keywords = {Electronic contracts, Kleene algebra, guarded rooted trees, concurrency, completeness},
pdf = {publications/TR361.pdf}
}
@techreport{PS07tr1,
key = {TechRep},
title = {Towards a {F}ormal {D}efinition of {E}lectronic {C}ontracts},
author = {Prisacariu, Cristian and Schneider, Gerardo},
publisher = {Department of Informatics, University of Oslo},
address = {Oslo, Norway},
pages = {52},
number = {348},
year = 2007,
month = {January},
abstract = {In this paper we propose a formal language for writing electronic contracts, based on the normative deontic notions of obligation, prohibition, and permission. We take an ought-to-do approach, where the above notions are applied to actions instead of state-of-affairs. We propose an extension of the mu-calculus in order to capture the intuitive meaning of obligation, prohibition and permission, and to express deterministic and concurrent actions. We provide a translation of the contract language into the logic, and we show how the semantics faithfully captures the meaning of the contract language. We also show how our language captures most of the intuitive desirable properties of electronic contracts, as well as how it avoids most of the classical paradoxes of deontic logic. We also discuss informally the main problems in formalizing the above normative deontic notions in particular in the context of electronic contracts. We finally show its applicability on a contract example.},
institution = {Department of Informatics, University of Oslo},
keywords = {Electronic contracts, mu-calculus, deontic logic, concurrency},
pdf = {publications/TR348.pdf}
}
@inproceedings{O9icsoc,
key = {other},
title = {{Analyzing Orchestration of BPEL Specified Services with Model Checking}},
author = {Joseph C. Okika},
booktitle = {Proceedings of the PhD Symposium of the 7th International Joint Conference on Service Oriented Computing (ICSOC/ServiceWave)},
opteditor = {Michael R. Hansen and Aske Brekling},
optpublisher = {DTU Informatics},
optaddress = {Oslo, Norway},
pages = {1-6},
year = 2009,
month = {July},
optpdf = {papers/nwpt00OOP.pdf},
optps = {papers/nwpt09OOP.ps}
}
@inproceedings{OR07flacos,
key = {other},
title = {{Compositionality and Compatibility of Service Contracts}},
author = {Joseph C. Okika and Anders P. Ravn},
booktitle = {NWPT'07/FLACOS'07 Workshop Proceeding},
opteditor = {Michael R. Hansen and Aske Brekling},
optpublisher = {DTU Informatics},
address = {Oslo, Norway},
pages = {101-103},
year = 2007,
month = {October},
optpdf = {papers/nwpt00OOP.pdf},
optps = {papers/nwpt09OOP.ps}
}
@inproceedings{P10yrfmfcsl,
key = {other},
title = {{Modal Logic over Higher Dimensional Automata (extended abstract)}},
author = {Cristian Prisacariu},
booktitle = {Young Researchers Forum at Mathematical Foundations of Computer Science (YRF@MFCS'10)},
editor = {Jan Strejcek},
optpublisher = {DTU Informatics},
address = {Brno, Czech Republic},
oppages = {95-98},
year = 2010,
optisbn = {978-87-643-0565-4},
month = {August},
pdf = {publications/yrfmfcs10.pdf},
ps = {publications/yrfmfcs10.ps},
keywords = {higher dimensional automata, Mazurkiewicz trace theory, event structures, linear temporal logic, LTrL, modal logic, 'during' modality, axiomatization completeness and decidability, filtration},
optabstract = {}
}
@inproceedings{BP10unif,
key = {other},
title = {{Unification and Matching in Separable Theories (extended abstract)}},
author = {Sergiu Bursuc and Cristian Prisacariu},
booktitle = {24th International Workshop on Unification (UNIF10)},
editor = {Maribel Fernandez},
optpublisher = {DTU Informatics},
address = {Edimburg, UK},
oppages = {95-98},
year = 2010,
optisbn = {978-87-643-0565-4},
month = {July},
pdf = {publications/unif10.pdf},
ps = {publications/unif10.ps},
keywords = {Unification, matching, semirings, idempotent semirings, separability, stratification, equational theories},
abstract = {We study problems of unification and matching in equational theories based on semirings. These theories include Kleene algebra and its extensions with different forms of concurrency, constraint semirings, and synchronous actions algebra. Generally the unification problems are undecidable in this setting, but different undecidability proofs are required. On the other hand, the matching problems are decidable and a general pattern can be drawn. This pattern is developed into a matching algorithm, relying on a new way of combining non-disjoint theories, which we call stratification, and on a relaxation of the finite variant property, which we call separability. Consequently, we believe that our algorithm and the notions that we introduce have an importance i) beyond theories based on semirings; ii) for other problems related to unification and matching.}
}
@inproceedings{OOP09nwpt,
key = {other},
title = {{Operational Semantics for BPEL Complex Features in Rewriting Logic (extended abstract)}},
author = {Joseph C. Okika and Olaf Owe and Cristian Prisacariu},
booktitle = {21st Nordic Workshop on Programming Theory (NWPT09)},
editor = {Michael R. Hansen and Aske Brekling},
publisher = {DTU Informatics},
address = {Lyngby, Denmark},
pages = {95-98},
year = 2009,
isbn = {978-87-643-0565-4},
month = {October},
pdf = {publications/nwpt00OOP.pdf},
ps = {publications/nwpt09OOP.ps},
keywords = {BPEL language, rewriting logic, operational semantics, concurrency, compensations},
abstract = {In our work we take an operational semantics approach and formalize some of the complex features of BPEL based on rewriting logic. The advantage of this approach is that the semantics is now executable in Maude. This caters for analyses of BPEL processes using simulation and for verification using breath-first search.}
}
@inproceedings{P09nwpt,
key = {other},
title = {{A Decidable Logic for Complex Contracts (extended abstract)}},
author = {Cristian Prisacariu},
booktitle = {21st Nordic Workshop on Programming Theory (NWPT09)},
editor = {Michael R. Hansen and Aske Brekling},
publisher = {DTU Informatics},
address = {Lyngby, Denmark},
pages = {65-68},
year = 2009,
isbn = {978-87-643-0565-4},
month = {October},
pdf = {publications/nwpt09.pdf},
ps = {publications/nwpt09.ps},
keywords = {contracts, propositional dynamic logic, actions, synchrony model of concurrency, tree model property},
abstract = {The present abstract reports on the state-of-the-art of the logic for contracts CL, which we have been developing over the last few years. These research efforts have spread over several papers, which we summarize here. We present also some current work. The main motivation for our work is to have a logic which expresses, at an abstract level, complex behavior (of concurrent programs, of communicating intelligent agents, of web services, or of legal contracts; just to name a few possible concretizations of the behaviors we think of). The purpose of this logic is, not only, to formalize such behaviors, but mainly to reason about their formalizations. Therefore we seek a decidable logic, so to have hopes for automation; i.e., to do automated model checking and run-time monitoring.}
}
@inproceedings{P09YRconcur,
key = {other},
title = {{Synchronous Kleene Algebra vs. Concurrent Kleene Algebra}},
author = {Cristian Prisacariu},
booktitle = {Young Researchers Workshop on Concurrency Theory (YRCONCUR09)},
editor = {Joost-Pieter Katoen},
optpublisher = {},
address = {Bologna, Italy},
optpages = {},
year = 2009,
optisbn = {},
month = {September},
pdf = {publications/yrconcur09.pdf},
ps = {publications/yrconcur09.ps},
abstract = {In this year's CONCUR conference Concurrent Kleene Algebra (CKA) is presented as a general formalism for reasoning about concurrent programs. Also recently Synchronous Kleene Algebra (SKA) was investigated by this author with the purpose of representing and reasoning about actions/programs that have a notion of concurrency in the style of synchrony of the SCCS calculus. CKA has, at first sight, striking resemblances with SKA. We discuss this model of concurrency in relation with SKA. Our discussion focuses on the underlying ideas and intuitions of the two models. The discussion is also casted into the partial orders model of concurrency to get more insights into the two algebras.}
}
@inproceedings{PS09icail,
key = {other},
title = {{Abstract Specification of Legal Contracts}},
author = {Cristian Prisacariu and Gerardo Schneider},
booktitle = {12th International Conference on Artificial Intelligence and Law (ICAIL09)},
editor = {Carole Hafner},
publisher = {ACM Press},
address = {Barcelona, Spain},
pages = {218-219},
year = 2009,
isbn = {1-60558-597-0},
month = {June},
pdf = {publications/icail09.pdf},
ps = {publications/icail09.ps},
abstract = {The paper presents an action-based formal language called CL for abstract specification of legal contracts. The purpose of the language is to be used to reason about legal contracts (and electronic contracts on the long run). CL combines the legal notions obligation, permission, and prohibition from deontic logic with the action modality of propositional dynamic logic (PDL). The deontic modalities are applied only over actions, thus following the ought-to-do approach. The language includes a synchrony operator to model ``actions performed at the same time'', and a special complementation operation to encode the violation of obligations. The language has a formal semantics in terms of normative structures, specially defined to capture several natural properties of legal contracts. We focus on the informal presentation of the choices made when designing CL, and its semantics.},
keywords = {e-contracts, legal contracts, deontic logic, PDL, synchrony, semantics, normative structure, decidability},
doi = {10.1145/1568234.1568262}
}
@inproceedings{P08nwpt,
key = {other},
title = {{Extending Kleene Algebra with Synchrony: Completeness and Decidability (extended abstract)}},
author = {Cristian Prisacariu},
booktitle = {20th Nordic Workshop on Programming Theory (NWPT08)},
editor = {Tarmo Uustalu and Juri Vain},
optpublisher = {},
address = {Tallinn, Estonia},
optpages = {},
year = 2008,
optisbn = {},
month = {November},
pdf = {publications/nwpt08C.pdf},
abstract = {The work reported here investigates the introduction of synchrony into Kleene algebra. The resulting algebraic structure is called synchronous Kleene algebra. Models are given in terms of regular sets of concurrent strings and finite automata accepting concurrent strings. The extension of synchronous Kleene algebra with Boolean tests is presented together with models on regular sets of guarded concurrent strings and the associated automata on guarded concurrent strings. Completeness w.r.t. the standard interpretations is given in each case. Decidability follows from completeness.}
}
@inproceedings{FPS08cad,
key = {other},
author = {Stephen Fenech and Gordon J. Pace and Gerardo Schneider},
title = {{Conflict Analysis of Deontic Contracts}},
booktitle = {20th Nordic Workshop on Programming Theory (NWPT08)},
editor = {Tarmo Uustalu and Juri Vain},
optpublisher = {},
address = {Tallinn, Estonia},
optpages = {},
year = 2008,
optisbn = {},
month = {November},
pdf = {publications/nwpt08.pdf}
}
@inproceedings{P07calco_jnr,
key = {other},
title = {An {A}lgebraic {S}tructure for {C}oncurrent {A}ctions - abstract},
author = {Cristian Prisacariu},
booktitle = {CALCO jounior 07},
editor = {Magne Haveraaen and John Power and Monika Seisenberger},
optpublisher = {},
address = {Bergen, Norway},
optpages = {339--344},
year = 2007,
optisbn = {972-8865-69-4},
month = {August},
pdf = {publications/calco07.pdf},
optabstract = {}
}
@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob tmpbib.bib -c 'key : "Disemination"' bib.bib}}
@incollection{GOR+08cos,
key = {Disemination},
author = {Pablo Giambiagi and Olaf Owe and Anders P. Ravn and Gerardo Schneider},
title = {Contract-Oriented Software Development for Internet Services},
booktitle = {{ERCIM News magazine -- Special: The Future WEB}},
year = {2008},
month = {January},
number = {72},
pages = {47--48},
note = {{\url{http://ercim-news.ercim.org/images/stories/EN72/EN72-web.pdf}}},
abstract = {{COSoDIS (Contract-Oriented Software Development for Internet Services)} develops novel approaches to implement and reason about contracts in service oriented architectures (SOA). The rationale is that system developers benefit from abstraction mechanisms to work with these architectures. Therefore the goal is to design and test system modeling and programming language tools to empower SOA developers to deploy highly dynamic, negotiable and monitorable Internet services.},
pdf = {publications/ercim08.pdf}
}
@incollection{G08cource_africa,
key = {Disemination},
author = {Gerardo Schneider},
title = {Invited course on {\it Specification and verification of e-contracts}},
booktitle = {{the associated school to the 6th IEEE International Conference on Software Engineering and Formal Methods (SEFM School)}},
year = {2008},
address = {Cape Town, South Africa},
month = {November},
note = {{\url{http://www.iist.unu.edu/SEFM08/}}},
optabstract = {}
}