@inproceedings{RS13moa,
author = {Pavel Rabetski and Gerardo Schneider},
title = {MIgration of an on-premise application to the Cloud: Experience report},
optcrossref = {},
optkey = {},
booktitle = {European Conference on Service-Oriented and Cloud Computing (ESOCC'13)},
optpages = {},
year = {2013},
opteditor = {},
optvolume = {},
optnumber = {},
series = {LNCS},
address = {Malaga, Spain},
optmonth = {September},
optorganization = {},
optpublisher = {},
note = {To appear},
issn = {1567-8326},
isbn = {},
pdf = {esocc2013.pdf},
abstract = {As of today it is still not clear how and when cloud computing should be used.
Developers very often write applications in a way that does not really fit a cloud environment, and in some cases without taking into account how quality attributes (like performance, security or portability) are affected. In this paper we share our experience and observations from adopting cloud computing for an on-premise enterprise application in a context of a small software company. We present experimental results concerning a comparative evaluation (w.r.t. performance and cost) of the behavior of the original system both on-premise and on the Cloud, considering different scenarios in the Cloud.}
}
@article{ACS13fca,
author = {Krasimir Angelov and John C.~Camilleri and Gerardo Schneider},
title = {A Framework for Conflict Analysis of Normative Texts Written in Controlled Natural Language},
journal = {{Journal of Logic and Algebraic Programming}},
year = {2013},
optkey = {},
optvolume = {},
optnumber = {},
optpages = {},
optmonth = {},
issn = {1567-8326},
isbn = {},
url = {http://dx.doi.org/10.1016/j.jlap.2013.03.002},
publisher = {Elsevier},
pdf = {jlap13-CL_GF.pdf},
abstract = {In this paper we are concerned with the analysis of normative conflicts, or the detection of conflicting obligations, permissions and prohibitions in normative texts written in a Controlled Natural Language (CNL). For this we present \AnaCon, a proof-of-concept system where normative texts written in CNL are automatically translated into the formal language CL using the Grammatical Framework (GF). Such CL expressions are then analysed for normative conflicts by the CLAN tool, which gives counter-examples in cases where conflicts are found. The framework also uses GF to give a CNL version of the counter-example, helping the user to identify the conflicts in the original text. We detail the application of AnaCon to two case studies and discuss the effectiveness of our approach.},
note = {To appear}
}
@inproceedings{NST13atr,
author = {Robert Nagy and Gerardo Schneider and Aram Timofeitchik},
title = {Automatic Testing of Real-Time Graphics Systems},
booktitle = {{19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13)}},
pages = {465-479},
year = {2013},
opteditor = {N. Piterman and S. Smolka},
volume = {7795},
series = {LNCS},
address = {Rome, Italy},
abstract = {In this paper we deal with the general topic of verification of real-time graphic systems. In particular we present the Runtime Graphics Verification Framework (RUGVEF), where we combine techniques from runtime verification and image analysis to automate testing of graphic systems. We provide a proof of concept in the form of a case study, where RUGVEF is evaluated in an industrial setting to verify an on-air graphics playout system used by the Swedish Broadcasting Corporation. We report on experimental results from the evaluation, in particular the discovery of five previously unknown defects not been detected before.},
pdf = {tacas2013.pdf},
publisher = {Springer}
}
@inproceedings{schneider12tfa,
author = {Gerardo Schneider},
title = {Towards a Framework for Analyzing Normative Texts in Controlled Natural Language},
optcrossref = {},
optkey = {},
booktitle = {6th International Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS'12)},
optpages = {},
year = {2012},
opteditor = {},
optvolume = {},
optnumber = {},
series = {EPTCS},
address = {Bertinoro, Italy},
month = {19 September},
optorganization = {},
optpublisher = {},
issn = {2075-2180},
optnote = {To appear},
optannote = {}
}
@inproceedings{APS12uas,
author = {Wolfgang Ahrendt and Gordon J.~Pace and Gerardo Schneider},
title = {{A Unified Approach for Static and Runtime Verification: Framework and Applications}},
booktitle = {5th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'12) - Part I},
pages = {312-326},
year = {2012},
opteditor = {T.~Margaria and B.~Steffen and M.~Merten},
volume = {7609},
optnumber = {},
series = {LNCS},
address = {Heraclion, Crete},
month = {15-18 October},
optorganization = {},
publisher = {Springer},
url = {http://dx.doi.org/10.1007/978-3-642-34026-0_24},
pdf = {isola12.pdf},
abstract = {Static verification of software is becoming ever more effective and efficient. Still, static techniques either have high precision, in which case powerful judgements are hard to achieve automatically, or they use abstractions supporting increased automation, but possibly losing important aspects of the
concrete system in the process. Runtime verification has complementary strengths and weaknesses. It combines full precision of the model (including the real deployment environment) with full automation, but cannot judge future and alternative runs. Another drawback of runtime verification can be the computational
overhead of monitoring the running system which, although typically not very high, can still be prohibitive in certain settings. In this paper we propose a framework to combine static analysis techniques and runtime verification with the aim of getting the best of both techniques. In particular, we discuss an
instantiation of our framework for the deductive theorem prover KeY, and the runtime verification tool LARVA. Apart from combining static and dynamic verification, this approach also combines the data centric analysis of KeY with the control-centric analysis of LARVA. An advantage of the approach is that, through the use of a single specification which can be used by both analysis techniques, expensive parts of the analysis could be moved to the static phase, allowing the runtime monitor to make significant assumptions, dropping parts of expensive checks at runtime. We also discuss specific applications of our approach.},
optnote = {Track: Runtime Verification: the application perspective}
}
@proceedings{BS12flacos10,
title = {{Special Section: Formal Languages and Analysis of Contract-Oriented Software (FLACOS'10)}},
year = {2012},
editor = {Antonio Brogi and Gerardo Schneider},
volume = {81(2)},
number = {2},
series = {{Journal of Logic and Algebraic Programming}},
optaddress = {},
month = {February},
optorganization = {},
issn = {1567-8326},
isbn = {},
url = {http://dx.doi.org/10.1016/j.jlap.2011.12.003},
publisher = {Elsevier}
}
@article{HSS11rac,
author = {Hallstein Hansen and Gerardo Schneider and Martin Steffen},
title = {Reachability analysis of complex planar hybrid systems},
optmonth = {},
publisher = {Elsevier},
optvolume = {},
optnumber = {},
optpages = {},
year = {2013},
journal = {Science of Computer Programming (SCP)},
note = {To appear},
url = {http://dx.doi.org/10.1016/j.scico.2013.02.007},
issn = {},
isbn = {},
pdf = {scp2013.pdf},
abstract = {Hybrid systems are systems that exhibit both discrete and continuous
behavior. Reachability, the question of whether a system in one state can
reach some other state, is undecidable for hybrid systems in general. The
Generalized Polygonal Hybrid System (GSPDI) is a restricted form of hybrid
automaton where reachability is decidable. It is limited to two continuous
variables that uniquely determine which location the automaton is in, and
restricted in that the discrete transitions does not allow changes in the
state, only the location, of the automaton. One application of GSPDIs is
for approximating control systems and verifying the safety of such systems.
In this paper we present the following two contributions: i) An optimized
algorithm that answers reachability questions for GSPDIs, where all cycles
in the reachability graph are accelerated. ii) An algorithm by which more
complex planar hybrid systems are over-approximated by GSPDIs subject to
two measures of precision. We prove soundness, completeness, and
termination of both algorithms, and discuss their implementation.}
}
@techreport{HSS11racB,
author = {Hallstein Hansen and Gerardo Schneider and Martin Steffen},
title = {Reachability analysis of complex planar hybrid systems},
institution = {Department of Informatics, University of Oslo},
year = {2011},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
month = {November},
number = {412},
isbn = {82-7368-374-5},
issn = {0806-3036},
pdf = {report-UiO-412.pdf},
url = {http://urn.nb.no/URN:NBN:no-29825},
abstract = {Hybrid systems are systems that exhibit both discrete and continuous
behavior. Reachability, the question of whether a system in one state can
reach some other state, is undecidable for hybrid systems in general. The
Generalized Polygonal Hybrid System (GSPDI) is a restricted form of hybrid
automaton where reachability is decidable. It is limited to two continuous
variables that uniquely determine which location the automaton is in, and
restricted in that the discrete transitions does not allow changes in the
state, only the location, of the automaton. One application of GSPDIs is
for approximating control systems and verifying the safety of such systems.
In this paper we present the following two contributions: i) An optimized
algorithm that answers reachability questions for GSPDIs, where all cycles
in the reachability graph are accelerated. ii) An algorithm by which more
complex planar hybrid systems are over-approximated by GSPDIs subject to
two measures of precision. We prove soundness, completeness, and
termination of both algorithms, and discuss their implementation.}
}
@proceedings{BPSsefm11,
title = {{Software Engineering and Formal Methods}},
year = {2011},
editor = {Gilles Barthe and Alberto Pardo and Gerardo Schneider},
volume = {7041},
series = {{Lecture Notes in Computer Science}},
optaddress = {},
month = {November},
issn = {0302-9743},
isbn = {978-3-642-24689-0},
url = {http://dx.doi.org/10.1007/978-3-642-24690-6},
publisher = {Springer}
}
@inproceedings{MRS11fcs,
author = {Seyed M. Montazeri and Nivir Roy and Gerardo Schneider},
title = {{From Contracts in Structured English to CL Specifications}},
booktitle = {5th International Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS'11)},
pages = {55-69},
year = {2011},
opteditor = {},
volume = {68},
series = {EPTCS},
address = {M\'alaga, Spain},
month = {22-23 September},
optpublisher = {},
issn = {2075-2180},
isbn = {},
url = {http://dx.doi.org/10.4204/EPTCS.68.6},
pdf = {flacos11-GFCL.pdf},
abstract = {In this paper we present a framework to analyze conflicts of contracts written in structured English. A contract that has manually been rewritten in a structured English is automatically translated into a formal language using the Grammatical Framework (GF). In particular we use the contract language CL as a target formal language for this translation. In our framework CL specifications could then be input into the tool CLAN to detect the presence of conflicts (whether there are contradictory obligations, permissions, and prohibitions. We also use GF to get a version in (restricted) English of CL formulae. We discuss the implementation of such a framework.}
}
@inproceedings{MCD+11tas,
author = {Enrique Mart\'{i}nez and Mar\'{i}a E. Cambronero and Gregorio D\'{i}az and Gerardo Schneider},
title = {{Timed Automata Semantics for Visual e-Contracts}},
booktitle = {5th International Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS'11)},
pages = {7-21},
year = {2011},
opteditor = {},
volume = {68},
series = {EPTCS},
address = {M\'alaga, Spain},
month = {22-23 September},
optpublisher = {},
issn = {2075-2180},
isbn = {},
url = {http://dx.doi.org/10.4204/EPTCS.68.3},
pdf = {flacos11-CO.pdf},
abstract = {C-O Diagrams have been introduced as a means to have a more visual representation of electronic contracts, where it is possible to represent the obligations, permissions and prohibitions of the different signatories, as well as what are the penalties in case of not fulfillment of their obligations and prohibitions. In such diagrams we are also able to represent absolute and relative timing constraints. In this paper we present a formal semantics for C-O Diagrams based on timed automata extended with an ordering of states and edges in order to represent different deontic modalities.}
}
@proceedings{PS11flacos09,
title = {{Special Issue: Formal Languages and Analysis of Contract-Oriented Software}},
year = {2011},
editor = {Gordon Pace and Gerardo Schneider},
volume = {80(3-5)},
number = {3-5},
series = {{Journal of Logic and Algebraic Programming}},
optaddress = {},
month = {April-July},
optorganization = {},
issn = {1567-8326},
isbn = {},
url = {http://dx.doi.org/10.1016/j.jlap.2011.04.001},
publisher = {Elsevier}
}
@unpublished{BCG+11mrt,
author = {Ingram Bondin and Christian Colombo and Andrew Gauci and Gordon J. Pace and Gerardo Schneider},
title = {Monitoring Real-Time Properties with Overhead Guarantees},
optmonth = {},
optpublisher = {IEEE},
optvolume = {},
optnumber = {},
optpages = {},
year = {2011},
optjournal = {Transactions on Software Engineering},
note = {Submitted to IEEE Transactions on Software Engineering. Submitted Sep 2010; Revised Apr 2011},
issn = {},
isbn = {},
abstract = {Although the use of runtime verification has recently increased as a lightweight formal verification approach, major challenges still exist in applying such technique to real-time systems due to the overhead induced on the system by monitoring. In this paper, we focus on runtime monitoring of real-time properties and analysis to enable guarantees about the overheads induced through monitoring. In particular, we provide two types of guarantees: given a system property, we present an analysis to decide whether the property satisfaction or violation is affected by system slowdown or speedup, and for more stringent conditions, we enable guaranteeing an upper-bound on overhead incurred in monitoring a particular property. The framework is embodied in the tool LARVA, which we have extended to reason about statistical properties, and which has been applied to a number of industrial systems.}
}
@article{PS12ddl,
author = {Cristian Prisacariu and Gerardo Schneider},
title = {A Dynamic Deontic Logic for Complex Contracts},
optmonth = {},
publisher = {Elsevier},
volume = {81},
number = {4},
pages = {458-490},
month = {May},
year = {2012},
journal = {Journal of Logic and Algebraic Programming},
url = {http://dx.doi.org/10.1016/j.jlap.2012.03.003},
issn = {1567-8326},
isbn = {},
pdf = {jlap2012.pdf},
abstract = {We present a dynamic deontic logic for specifying and reasoning about complex contracts. The concepts that our contract logic CL captures are drawn from legal contracts, as we consider that these are more general and expressive that what is usually found in computer science (like in software contracts, web services specifications, or communication protocols). CL is intended to be used in specifying complex contracts found in computer science. This influences many of the design decisions behind CL. We adopt an ought-to-do approach to deontic logic and apply the deontic modalities exclusively over complex actions. We add the dynamic logic modality so to be able to reason about what happens after an action is performed. CL can reason about regular synchronous actions done at the same time. CL incorporates the notions of contrary-to-duty and contrary-to-prohibition by attaching to the deontic modalities explicitly a reparation which is to be enforced in case of violations. Results of decidability and tree model property are given as well as specific properties for the modalities.}
}
@inproceedings{HSS11ran,
author = {Hallstein A. Hansen and Gerardo Schneider and Martin Steffen},
title = {{Reachability analysis of non-linear planar autonomous systems}},
booktitle = {Fourth International Conference on Fundamentals of Software Engineering (FSEN'11)},
pages = {206-220},
year = {2012},
editor = {F. Arbab and M. Sirjani},
volume = {7141},
series = {LNCS},
address = {Teheran, Iran},
month = {20-22 April},
publisher = {Springer},
issn = {0302-9743},
isbn = {},
url = {http://dx.doi.org//10.1007/978-3-642-29320-7_14},
pdf = {fsen2011.pdf},
abstract = {Many complex continuous systems are modeled as non-linear autonomous
systems, i.e., by a set of differential equations with one independent
variable. Exact reachability, i.e., whether a given configuration
can be reached by starting from an initial configuration of the system,
is undecidable in general, as one needs to know the solution of the
system of equations under consideration.
In this paper we address the reachability problem of planar autonomous
systems approximatively. We use an approximation technique which
"hybridizes" the state space in the following way: the original system
is partitioned into a finite set of polygonal regions where the dynamics
on each region is approximated by constant differential
inclusions. Besides proving soundness, completeness, and termination of
our algorithm, we present an implementation, and its application into
(classical) examples taken from the literature.}
}
@inproceedings{MS10avs,
author = {Enrique Martinez and Gerardo Schneider},
title = {{Automated Analysis of Conflicts in Software Product Lines}},
booktitle = {1st International Workshop on Formal Methods in Software Product Line Engineering (FMSPLE'10)},
optpages = {},
year = {2010},
opteditor = {},
optvolume = {},
address = {Jeju Island, South Korea},
month = {September},
optpublisher = {},
issn = {},
isbn = {},
opturl = {http://dx.doi.org/},
pdf = {FMSPLE10.pdf},
abstract = {In this paper we propose a framework where the behaviour of features can be modelled using a visual model language for contracts (C-O Diagrams). We present a partial translation from C-O Diagrams into the deontic contract language CL allowing to detect whether there are contradicting features, using the tool CLAN. We aim at handling conflicts arising from software evolution and variability. As a proof of concept we apply our technique to a trading system case study.}
}
@inproceedings{MCD+,
author = {Enrique Martinez and Emilia Cambronero and Gregorio Diaz and Gerardo Schneider},
title = {{A Model for Visual Specification of e-Contracts}},
booktitle = {The 7th IEEE International Conference on Services Computing (IEEE SCC'10)},
pages = {1--8},
year = {2010},
opteditor = {},
optvolume = {},
address = {Miami, USA},
month = {July 5--10},
publisher = {IEEE Computer Society},
issn = {},
isbn = {978-0-7695-4126-6},
url = {http://dx.doi.org/10.1109/SCC.2010.32},
pdf = {scc2010.pdf},
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.}
}
@techreport{PS09flacos,
author = {Gordon J. Pace and Gerardo Schneider},
title = {{FLACOS'09 Workshop Proceedings}},
institution = {Department of Informatics, University of Oslo},
year = {2009},
number = {385},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
isbn = {82-7368-345-1},
issn = {0806-3036},
month = {September},
note = {Editors},
pdf = {report-UiO-385.pdf}
}
@techreport{CPS09rbr,
author = {Christian Colombo and Gordon Pace and Gerardo Schneider},
title = {Resource-bounded runtime verification of Java programs with real-time properties},
institution = {Department of Computer Science, University of Malta},
year = {2009},
number = {CS2009-01},
month = {December},
pdf = {report-Malta-CS2009-01.pdf},
abstract = {Given the intractability of exhaustively verifying software, the use
of runtime verification, to verify single execution paths at runtime,
is becoming increasingly popular. Undoubtedly, the overhead introduced
by runtime verification is a concern for system developers planning to
introduce this technique in their work. By using Lustre to write
security-critical properties, we exploit the language's guarantees on
bounded resources. We translate these properties into the existing
monitoring framework LARVA, making monitoring of programs
both easily applicable to Java programs and at the same time
guaranteed to use bounded-resources.
We use a subset of Quantified Discrete-time Duration Calculus (QDDC)
as an alternative specification notation for real-time
properties because it is translatable into Lustre.
Thus, QDDC also enjoys the same guarantees given when using Lustre.}
}
@inproceedings{HS10rag,
author = {Hallstein A. Hansen and Gerardo Schneider},
title = {{Reachability Analysis of GSPDIs: Theory, Optimization, and
Implementation}},
booktitle = {25th Annual ACM Symposium on Applied Computing --Software Verification and Testing track (SAC-SVT'10)},
pages = {2511-2516},
year = {2010},
opteditor = {Sung Y. Shin and Sascha Ossowski and Michael Schumacher and Mathew J. Palakal and Chih-Cheng Hung},
address = {Sierre, Switzerland},
month = {March 22-26},
publisher = {ACM},
url = {http://dx.doi.org/10.1145/1774088.1774609},
issn = {},
isbn = {978-1-60558-639-7},
abstract = {Analysis of systems containing both discrete and continuous dynamics,
hybrid systems, is a difficult issue. Most problems have been shown
to be undecidable, with the exception of a few classes where the dynamics are
restricted and/or the dimension is low. In this paper we present some
theoretical results concerning the decidability of the reachability
problem for a class of planar hybrid systems called Generalized
Polygonal Hybrid Systems (GSPDI). These new results provide means to
optimize a previous reachability algorithm, making the implementation
feasible. We also discuss the implementation of the algorithm into a
tool.},
pdf = {sac10.pdf}
}
@booklet{HS09ora,
author = {Hallstein A. Hansen and Gerardo Schneider},
title = {{On the reachability analysis of planar, non-linear autonomous systems using hybrid systems}},
howpublished = {NWPT'09},
address = {Lyngby, Denmark},
month = {October},
year = {2009},
note = {Extended Abstract},
pdf = {nwpt09.pdf}
}
@misc{BPS09cel,
author = {Gilles Barthe and Gordon J. Pace and Gerardo Schneider},
title = {Contract Embedded Languages for Services},
note = {In preparation},
year = {2009},
issn = {},
isbn = {},
abstract = {}
}
@inproceedings{FPS09ctc,
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)},
pages = {90--96},
year = {2009},
opteditor = {Zhiming Liu and Anders P. Ravn},
volume = {5799},
series = {LNCS},
address = {Macao, China},
month = {October},
publisher = {Springer},
url = {http://dx.doi.org/10.1007/978-3-642-04761-9_8},
pdf = {atva09.pdf},
issn = {0302-9743},
isbn = {978-3-642-04760-2},
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.}
}
@article{AMP+07,
author = {Eugene Asarin and Venkatesh Mysore and Amir Pnueli and Gerardo Schneider},
title = {Low Dimensional Hybrid Systems - Decidable, Undecidable, Don't Know},
journal = {Information and Computation},
publisher = {Elsevier},
volume = {211},
optnumber = {},
pages = {138-159},
month = {January},
year = {2012},
optnote = {Submitted Jun 2009, Revised Jun 2011, Accepted Nov 2011, Final Version Dec 2011},
issn = {0890-5401},
isbn = {},
url = {http://dx.doi.org/10.1016/j.ic.2011.11.006},
pdf = {infcomp2012.pdf},
abstract = {Even though many attempts have been made to define the boundary between
decidable and undecidable hybrid systems, the affair is far from being
solved. More and more low dimensional systems are being shown to be
undecidable with respect to reachability, and many open problems in
between are being discovered. In this paper, we present various two
dimensional hybrid systems for which the reachability problem is
undecidable. We show their undecidability by simulating
Minsky machines. Their proximity to the decidability frontier is
understood by inspecting the most parsimonious constraints necessary
to make reachability over these automata decidable. We also show that
for other two dimensional systems, the reachability
question remains unanswered, by proving that it is as hard as the
reachability problem for piecewise affine maps on the real line, which is a well known open problem.}
}
@inproceedings{APSY02svt,
author = {Eugene Asarin and Gordon Pace and Gerardo Schneider and Sergio Yovine},
title = {{SPeeDI}: a verification tool for polygonal hybrid systems},
booktitle = {Computer Aided Verification (CAV'02)},
pages = {354--358},
year = {2002},
opteditor = {E. Brinksma and K.G. Larsen },
volume = {2404},
series = {LNCS},
address = {Copenhagen, Denmark},
month = {July},
publisher = {Springer-Verlag},
url = {http://dx.doi.org/10.1007/3-540-45657-0_28},
pdf = {cav2002.pdf},
issn = {0302-9743},
isbn = {978-3-642-03465-7},
abstract = {We present SPeeDI, a tool for reachability analysis of Polygonal Hybrid Systems (SPDIs)}
}
@article{APSY07tcs,
author = {Eugene Asarin and Gordon Pace and Gerardo Schneider and Sergio Yovine},
title = {{Algorithmic Analysis of Polygonal Hybrid Systems. Part II: Phase Portrait and Tools}},
journal = {Theoretical Computer Science},
publisher = {Elsevier},
year = {2008},
volume = {390},
number = {1},
pages = {1--26},
month = {January},
url = {http://dx.doi.org/10.1016/j.tcs.2007.09.025},
issn = {0304-3975},
isbn = {},
abstract = {Polygonal differential inclusion systems (SPDI) are a subclass of planar hybrid automata which can be represented by piecewise constant differential inclusions. The reachability problem as well as the computation of certain objects of the phase portrait is decidable. In this paper we show how to compute the viability, controllability and invariance kernels, as well as semi-separatrix curves for SPDIs. We also present the tool SPeeDI+, which implements a DFS reachability algorithm and the phase portrait computation for SPDIs.},
pdf = {tcs07-2.pdf}
}
@inproceedings{AS02wgb,
author = {Eugene Asarin and Gerardo Schneider},
title = {Widening the boundary between decidable and undecidable hybrid systems},
booktitle = {13th International Conference on Concurrency Theory (CONCUR'02)},
pages = {193--208},
year = {2002},
opteditor = {L. Brim and P. Jancar and M. Kretinsky and A. Kucera},
volume = {2421},
series = {LNCS},
address = {Brno, Czech Republic},
month = {August},
publisher = {Springer-Verlag},
url = {http://dx.doi.org/10.1007/3-540-45694-5_14},
pdf = {concur2002.pdf},
issn = {0302-9743},
isbn = {3-540-44043-7 },
abstract = {We revisited decidability of the reachability problem for low
dimensional hybrid systems. Even though many attempts have been
done to draw the boundary between decidable and undecidable hybrid
systems there are still many open problems in between. In this
paper we show that the reachability question for some two
dimensional hybrid systems are undecidable and that for other
2-dim systems this question remains unanswered, showing that it is
as hard as the reachability problem for Piecewise Affine Maps,
that is a well known open problem.}
}
@inproceedings{ASY01drp,
author = {Eugene Asarin and Gerardo Schneider and Sergio Yovine},
title = {On the decidability of the reachability problem for planar differential inclusions},
booktitle = {4th International Workshop on Hybrid Systems: Computation and Control (HSCC'01)},
pages = {89--104},
year = {2001},
opteditor = {M.D.~di Benedetto and A.~Sangiovanni-Vincentelli},
number = {2034},
series = {LNCS},
address = {Rome, Italy},
publisher = {Springer-Verlag},
url = {http://dx.doi.org/10.1007/3-540-45351-2_11},
pdf = {hs2001.pdf},
issn = {0302-9743},
isbn = {3-540-41866-0},
abstract = { In this paper we develop an algorithm for solving the reachability
problem of two-dimensional piece-wise rectangular differential
inclusions. Our procedure is not based on the computation of the
reach-set but rather on the computation of the limit of individual
trajectories. A key idea is the use of one-dimensional affine
Poincaré maps for which we can easily compute the fixpoints. As a
first step, we show that between any two points linked by an
arbitrary trajectory there always exists a trajectory without
self-crossings. Thus, solving the reachability problem requires
considering only those. We prove that, indeed, there are only
finitely many ``qualitative types'' of those trajectories. The last
step consists in giving a decision procedure for each of them.
These procedures are essentially based on the analysis of the limits
of extreme trajectories. We illustrate our algorithm on a simple
model of a swimmer spinning around a whirlpool.}
}
@techreport{ASY01tr,
author = {Eugene Asarin and Gerardo Schneider and Sergio Yovine},
title = {{On the decidability of the reachability problem for planar differential inclusions}},
institution = {VERIMAG},
year = {2001},
address = {Grenoble, France},
month = {January},
ps = {hs2001_ext.ps.gz},
issn = {},
isbn = {},
abstract = {This is an extended version of the HSCC'2001 paper.}
}
@inproceedings{ASY02tcp,
author = {Eugene Asarin and Gerardo Schneider and Sergio Yovine},
title = {Towards Computing Phase Portraits of Polygonal Differential Inclusions},
booktitle = {5th International Workshop on Hybrid Systems: Computation and Control (HSCC'02)},
pages = {49--61},
year = {2002},
opteditor = {C.J. Tomlin and M.R. Greenstreet},
number = {2289},
series = {LNCS},
address = {Stanford, USA},
month = {March},
publisher = {Springer-Verlag},
url = {http://dx.doi.org/10.1007/3-540-45873-5_7},
pdf = {hs2002.pdf},
issn = {0302-9743},
isbn = {3-540-43321-X},
abstract = {Polygonal hybrid systems are a subclass of planar hybrid automata
which can be represented by piecewise constant differential
inclusions. Here, we study the problem of defining and constructing
the phase portrait of such systems. We identify various important
elements of it, such as viability and controllability kernels, and
propose an algorithm for computing them all. The algorithm is based on
a geometric analysis of trajectories.}
}
@article{ASY07tcs1,
author = {Eugene Asarin and Gerardo Schneider and Sergio Yovine},
title = {{Algorithmic Analysis of Polygonal Hybrid Systems. Part I: Reachability}},
journal = {Theoretical Computer Science},
publisher = {Elsevier},
year = {2007},
volume = {379},
number = {1-2},
pages = {231--265},
optmonth = {},
url = {http://dx.doi.org/10.1016/j.tcs.2007.03.055},
issn = {0304-3975},
isbn = {},
abstract = {In this work we are concerned with the formal verification of
two-dimensional non-deterministic hybrid systems, namely
polygonal differential inclusion systems (SPDIs). SPDIs are a
class of nondeterministic systems that correspond to piecewise
constant differential inclusions on the plane, for which we study
the reachability problem.
Our contribution is the development of an algorithm for solving
exactly the reachability problem of SPDIs. We extend
the geometric approach due to Maler and Pnueli
to non-deterministic systems, based on the combination of three techniques: the
representation of the two-dimensional continuous-time dynamics as a
one-dimensional discrete-time system (using Poincar\'e maps), the
characterization of the set of qualitative behaviors of the latter
as a finite set of types of signatures, and acceleration used
to explore reachability according to each of these types.
},
pdf = {tcs07.pdf}
}
@techreport{BMS04bfs,
author = {Michael Baldamus and Richard Mayr and Gerardo Schneider},
title = {A backward/forward strategy for verifying safety properties of infinite-state systems},
institution = {Department of Information Technology, Uppsala University},
year = {2004},
number = {2003-065},
month = {January},
pdf = {tech_rep_2003-065.pdf},
issn = {},
isbn = {},
abstract = { This paper has two main contributions: For one,
we describe a general method for verifying safety properties of
non--well--quasi--ordered infinite--state systems
for which reachability is undecidable in general, the
question being whether a set $U$ of configurations is
reachable. In many cases this problem can be solved as follows: First,
one constructs a well--quasi--ordered overapproximation of the system in question.
Thereby one can compute an
overapproximation of the set $\mathit{Pre}^*(U)$ of all predecessors of $U$.
Second, one performs an exact bounded forward search for $U$ (starting
at the initial state) which always stays
inside the already computed overapproximation of $\mathit{Pre}^*(U)$, thus
curbing the search space. This restricted
forward search is more efficient than a normal forward search,
yielding answers of the form YES, NO, or UNKNOWN,
where the YES and NO answers are always correct.
As our second main contribution herein, we apply
our method to relabelling--free CCS with finite sums,
which is already a process calculus
for which reachability is undecidable. To our knowledge,
this part is actually the first application of well--structered systems
to verifying safety properties in process calculi. The application
is done via a special Petri nets semantics for the calculus that we
consider.}
}
@inproceedings{BPS05pam,
author = {Gilles Barthe and Mariela Pavlova and Gerardo Schneider.},
title = {Precise analysis of memory consumption using program logics},
booktitle = {3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM'05)},
pages = {86--95},
year = {2005},
address = {Koblenz, Germany},
month = {September},
publisher = {IEEE Computer Society},
pdf = {sefm2005.pdf},
url = {http://dx.doi.org/10.1109/SEFM.2005.34},
issn = {},
isbn = {0-7695-2435-4},
abstract = {Memory consumption policies provide a means to control
resource usage on constrained devices, and play an important role
in ensuring the overall quality of software systems, and in
particular resistance against resource exhaustion attacks. Such
memory consumption policies have been previously enforced through
static analysis, which yield automatic bounds at the
cost of precision, or run-time analysis, which incur an overhead
that is not acceptable for constrained devices.
In this paper, we study the use of logical methods to specify and
statically verify precise memory consumption policies for Java
bytecode programs. First, we demonstrate how the Bytecode Specification
Language (a variant of the Java Modelling Language tailored to
bytecode) can be used to specify precise memory consumption policies
for (sequential) Java applets, and how verification tools can
be used to enforce such memory consumption policies. Second, we
consider the issue of inferring some of the annotations required to
express the memory consumption policy, and report on an inference
algorithm.
Our broad conclusion is that logical methods provide a suitable means
to specify and verify expressive memory consumption policies, with an
acceptable overhead.}
}
@inproceedings{CJPS05cmu,
author = {David Cachera and Thomas Jensen and David Pichardie and Gerardo Schneider},
title = {Certified memory usage analysis},
booktitle = {Formal Methods (FM'05)},
pages = {91--106},
series = {LNCS},
year = {2005},
volume = {3582},
address = {Newcastle Upon Tyne, UK},
month = {July},
publisher = {Springer-Verlag},
pdf = {fm2005.pdf},
url = {http://dx.doi.org/10.1007/11526841_8},
issn = {0302-9743},
isbn = {978-3-540-27882-5},
abstract = {We present a certified algorithm for resource usage analysis,
applicable to languages in the style of Java byte code. The algorithm
verifies that a program executes in bounded memory. The algorithm is
destined to be used in the development process of applets and for
enhanced byte code verification on embedded devices. We have therefore
aimed at a low-complexity algorithm derived from a loop detection
algorithm for control flow graphs. The expression of the algorithm as
a constraint-based static analysis of the program over simple lattices
provides a link with abstract interpretation that allows to state and
prove formally the correctness of the analysis with respect to an
operational semantics of the program. The certification is based on an
abstract interpretation framework implemented in the Coq proof
assistant which has been used to provide a complete formalisation and
formal verification of all correctness proofs.}
}
@inproceedings{CPS08lrt,
author = {Christian Colombo and Gordon J. Pace and Gerardo Schneider},
title = {Dynamic Event-Based Runtime Monitoring of Real-Time and Contextual Properties},
year = {2009},
month = {September},
booktitle = {{13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'08)}},
pages = {135--149},
opteditor = {},
volume = {5596},
series = {LNCS},
address = {L'Aquila, Italy},
publisher = {Springer-Verlag},
pdf = {fmics2008.pdf},
url = {http://dx.doi.org/10.1007/978-3-642-03240-0_13},
issn = {0302-9743},
isbn = {978-3-642-03239-4},
abstract = {Given the intractability of exhaustively verifying software, the use of runtime-verification, to verify single execution paths at runtime, is becoming popular. Although the use of runtime verification is increasing in industrial settings, various challenges still are to be faced to enable it to spread further. We present dynamic communicating automata with timers and events to describe properties of systems, implemented in LARVA, an event-based runtime verification tool for monitoring temporal and contextual properties of Java programs. The combination of timers with dynamic automata enables the straightforward expression of various properties, including replication of properties, as illustrated in the use of LARVA for the runtime monitoring of a real life case study --- an online transaction system for credit card. The features of LARVA are also benchmarked and compared to a number of other runtime verification tools, to assess their respective strengths in property expressivity and overheads induced through monitoring.}
}
@inproceedings{CPS08sir,
author = {Christian Colombo and Gordon J. Pace and Gerardo Schneider},
title = {Safe Runtime Verification of Real-Time Properties},
year = {2009},
booktitle = {The 7th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'09)},
pages = {103--117},
editor = {Joel Ouaknine and Frits Vaandrager},
volume = {5813},
series = {LNCS},
address = {Budapest, Hungary},
month = {13-16 September},
publisher = {Springer},
pdf = {formats2009.pdf},
url = {http://dx.doi.org/10.1007/978-3-642-04368-0_10},
issn = {0302-9743},
isbn = {978-3-642-04367-3},
abstract = {Introducing a monitor on a system typically changes the system's behaviour, whether it is slowing the system down, and increasing memory consumption. This may possibly result in creating bugs not in the original system, or possibly even "fixing" bugs, only to reappear as the monitor is removed. Properties written in a real-time logic, such as duration calculus, can be particularly sensitive to such changes induced through monitoring. In this paper, we identify a class of real-time properties, in duration calculus, which are monotonic under the slowing down (speeding up) of the underlying system. We apply this approach to the real-time runtime monitoring tool LARVA, where we use duration calculus as a monitoring property specification language, so we automatically identify properties which can be shown to be monotonic with respect to system re-timing.}
}
@inproceedings{CPS09ltr,
author = {Christian Colombo and Gordon J. Pace and Gerardo Schneider},
title = {{LARVA --A Tool for Runtime Monitoring of Java Programs}},
booktitle = {7th IEEE International Conference on Software Engineering and Formal Methods (SEFM'09)},
pages = {33--37},
year = {2009},
address = {Hanoi, Vietnam},
month = {23--27 November},
publisher = {IEEE Computer Society},
pdf = {sefm2009.pdf},
url = {http://dx.doi.org/10.1109/SEFM.2009.13},
issn = {},
isbn = {978-0-7695-3870-9},
abstract = {The use of runtime verification, as a lightweight approach to guarantee properties of systems, has been increasingly employed on real-life software. In this paper, we present a tool LARVA, for the runtime verification of real-time properties of Java programs. Properties can be expressed in a number of notations, including timed-automata enriched with stopwatches, Lustre, and a subset of duration calculus. The tool has been successfully used on a number of case-studies, including an industrial system handling financial transactions. LARVA also performs analysis of real-time properties, to calculate, if possible, an upper-bound on the memory and temporal overheads induced by monitoring. Moreover, it gives other useful information, as for instance what is the impact of monitoring the system with respect to the monitored properties.}
}
@inproceedings{FOP+08bsc,
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)},
pages = {39--55},
series = {ENTCS},
volume = {253},
number = {1},
address = {York, UK},
year = {2009},
month = {March},
url = {http://dx.doi.org/10.1016/j.entcs.2009.09.027},
issn = {1571-0661},
isbn = {},
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 = {fesca09-cocome.pdf}
}
@booklet{FPS08cad,
author = {Stephen Fenech and Gordon J. Pace and Gerardo Schneider},
title = {{Conflict Analysis of Deontic Contracts}},
howpublished = {NWPT'08},
address = {Tallinn, Estonia},
month = {November 19--21},
year = {2008},
note = {Extended Abstract},
pdf = {nwpt08.pdf}
}
@inproceedings{FPS09acd,
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)},
pages = {200--214},
year = {2009},
opteditor = {},
volume = {5684},
series = {LNCS},
address = {Kuala Lumpur, Malaysia},
month = {August},
publisher = {Springer},
url = {http://dx.doi.org/10.1007/978-3-642-03466-4_13},
issn = {0302-9743},
isbn = {978-3-642-03465-7},
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.},
pdf = {ictac09-contracts.pdf}
}
@incollection{GOR+07cos,
author = {Pablo Giambiagi and Olaf Owe and Anders P. Ravn and Gerardo Schneider},
title = {Contract-Oriented Software Development for Internet Services},
booktitle = {{ERCIM News -- Special: The Future WEB}},
year = {2008},
month = {January},
number = {72},
pages = {47--48},
url = {http://ercim-news.ercim.org/images/stories/EN72/EN72-web.pdf},
issn = {},
isbn = {},
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 = {ercim08.pdf}
}
@techreport{GOSR06cbi,
author = {Pablo Giambiagi and Olaf Owe and Anders P. Ravn and Gerardo Schneider},
title = {Contract-based Internet Service Software Development: A Proposal},
institution = {Department of Informatics, University of Oslo},
year = {2006},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
month = {January},
number = {333},
isbn = {82-7368-288-9},
issn = {0806-3036},
pdf = {report-UiO-333.pdf},
issn = {0806-3036},
isbn = {},
abstract = {The fast evolution of the Internet has popularized service-oriented architectures dynamic IT-supported inter-business collaborations. Yet, 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 proposes new language-based solutions to the above problem. Contracts are formalized as behavioral interfaces, and abstraction mechanisms may guide the developer in the production of contract-aware applications. We concentrate on contracts dealing with performance (real-time) and information flow (confidentiality).}
}
@inproceedings{GOSR06lbs,
author = {Pablo Giambiagi and Olaf Owe and Anders P. Ravn and Gerardo Schneider},
title = {Language-based Support for Service Oriented Architectures: Future Directions},
booktitle = {International Conference on Software and Data Technologies (ICSOFT'06)},
pages = {339--344},
year = {2006},
opteditor = {Joaquim Filipe and Boris Shishkov and Markus Helfert},
address = {Set\'ubal, Portugal},
month = {September},
optorganization = {},
publisher = {INSTICC Press},
opturl = {http://dx.doi.org/},
isbn = {972-8865-69-4},
pdf = {icsoft2006.pdf},
issn = {},
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.}
}
@inproceedings{GS05mca,
author = {Pablo Giambiagi and Gerardo Schneider},
title = {Memory consumption analysis of Java smart cards},
booktitle = {Proceedings of CLEI'05},
year = {2005},
address = {Cali, Colombia},
month = {October},
optpublisher = {Pontificia Universidad Javeriana Cali},
pdf = {clei2005.pdf},
opturl = {http://dx.doi.org/},
issn = {},
isbn = {958-670-426-2},
abstract = {Memory is a scarce resource in Java smart cards. Developers and card
suppliers alike would want to make sure, at compile- or load-time,
that a Java Card applet will not overflow memory when performing
dynamic class instantiations. Although there are good solutions to
the general problem, the challenge is still out to produce a static
analyser that is certified and could execute on-card. We provide a
constraint-based algorithm which determines potential loops and
(mutually) recursive methods. The algorithm operates on the bytecode
of an applet and is written as a set of rules associating one or
more constraints to each bytecode instruction. The rules are
designed so that a certified analyser could be extracted from their
proof of correctness. By keeping a clear separation between the
rules dealing with the inter- and intra-procedural aspects of the
analysis we are able to reduce the space-complexity of a previous
algorithm.}
}
@booklet{GSV03nsi,
title = {A note on scope and infinite behaviour in {CCS}-like calculi},
author = {Pablo Giambiagi and Gerardo Schneider and Frank D. Valencia},
howpublished = {NWPT'2003},
address = {Turku, Finland},
month = {October 29--31},
year = {2003},
note = {Extended Abstract},
ps = {nwpt03_ccs.ps.gz}
}
@techreport{GSV04ecc,
author = {Pablo Giambiagi and Gerardo Schneider and Frank D. Valencia},
title = {{On the expressiveness of CCS-like calculi}},
institution = {Department of Information Technology, Uppsala University},
year = {2004},
number = {2004-002},
address = {Sweden},
month = {January},
ps = {tec_rep_2004-002.ps.gz},
issn = {},
isbn = {},
abstract = {This an extended version of the FOSSACS 2004 paper.}
}
@inproceedings{GSV04eib,
author = {Pablo Giambiagi and Gerardo Schneider and Frank D. Valencia},
title = {On the expressiveness of infinite behavior and name scoping in process calculi},
booktitle = {Foundations of Software Science and Computation Structures (FOSSACS'04)},
pages = {226--240},
year = {2004},
volume = {2987},
series = {LNCS},
address = {Barcelone, Spain},
month = {March},
publisher = {Springer-Verlag},
pdf = {fossacs2004.pdf},
url = {http://dx.doi.org/10.1007/978-3-540-24727-2_17},
issn = {0302-9743},
isbn = {3-540-21298-1},
abstract = {In the literature there are several CCS-like process calculi
differing in the constructs for the specification of infinite
behavior and in the scoping rules for channel names. In this paper
we study various representatives of these calculi based upon both
their relative expressiveness and the decidability of
\emph{divergence}. We regard any two calculi as being \emph{equally
expressive} iff for every process in each calculus, there exists a
\emph{weakly bisimilar} process in the other.
By providing \emph{weak bisimilarity} preserving mappings among the
various variants, we show that in the context of
\emph{relabeling-free} and \emph{finite summation} calculi: (1) CCS
with \emph{parameterless} (or \emph{constant}) definitions is
equally expressive to the variant with \emph{parametric}
definitions. (2) The CCS variant with \emph{replication} is equally
expressive to that with \emph{recursive expressions} and
\emph{static} scoping. We also state that the divergence problem is
undecidable for the calculi in (1) but decidable for those in (2).
We obtain this from (un)decidability results by Busi, Gabbrielli and
Zavattaro, and by showing the relevant mappings to be computable and
to preserve divergence and its negation. From (1) and the
well-known fact that parametric definitions can replace injective
relabelings, we show that injective relabelings are redundant (i.e.,
derived) in CCS (which has constant definitions only).}
}
@inproceedings{HS07dpc,
author = {Johs H. Hammer and Gerardo Schneider},
title = {On the definition and policies of confidentiality},
booktitle = {3rd International Symposium on Information Assurance and Security (IAS'07)},
pages = {337-342},
year = {2007},
isbn = {0-7695-2876-7},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
address = {Manchester, UK},
month = {August},
publisher = {IEEE Computer Society Press},
url = {http://dx.doi.org/10.1109/IAS.2007.64},
issn = {},
isbn = {0-7695-2876-7},
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.},
pdf = {ias2007.pdf}
}
@inproceedings{HS09gta,
author = {Hallstein A. Hansen and Gerardo Schneider},
title = {{GSPeeDI --A Tool for Analyzing Generalized Polygonal Hybrid Systems}},
booktitle = {6th International Colloquium on Theoretical Aspects of Computing (ICTAC'09)},
pages = {336--342},
year = {2009},
opteditor = {},
volume = {5684},
series = {LNCS},
address = {Kuala Lumpur, Malaysia},
month = {August},
url = {http://dx.doi.org/10.1007/978-3-642-03466-4_23},
publisher = {Springer},
issn = {0302-9743},
isbn = {978-3-642-03465-7},
abstract = {The GSPeeDI tool implements a decision procedure for the reachability analysis of GSPDIs, planar hybrid systems whose dynamics is given by
differential inclusions, and that are not restricted by the goodness
assumption from previous work on the so-called SPDIs.
Unlike SPeeDI (a tool for reachability analysis of SPDI) the
underlying analysis of GSPeeDI is based on a breadth-first search
algorithm, and it can handle more general systems.},
pdf = {ictac09-GSPeeDI.pdf}
}
@techreport{JOS07nf,
author = {Einar B. Johnsen and Olaf Owe and Gerardo Schneider},
title = {{NWPT'07/FLACOS'07 Workshop Proceedings}},
institution = {Department of Informatics, University of Oslo},
year = {2007},
number = {366},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
isbn = {82-7368-324-9},
issn = {0806-3036},
month = {October},
note = {Editors},
pdf = {report-UiO-366.pdf}
}
@proceedings{JOS08nwpt,
title = {{Special Issue: The 19th Nordic Workshop on Programming Theory (NWPT 2007)}},
year = {2009},
editor = {Einar B. Johnsen and Olaf Owe and Gerardo Schneider},
volume = {78(7)},
number = {7},
series = {{Journal of Logic and Algebraic Programming}},
optaddress = {},
month = {August/September},
optorganization = {},
issn = {1567-8326},
isbn = {},
publisher = {Elsevier},
url = {http://dx.doi.org/10.1016/j.jlap.2009.06.001}
}
@inproceedings{JSO06rvc,
author = {Einar B. Johnsen and Gerardo Schneider and {\O}ystein Torget},
title = {Runtime Validation of Communication Histories},
booktitle = {IEEE 2nd International Conference on Intelligent Computer Communication and Processing (ICCP'06)},
pages = {161--168},
year = {2006},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
address = {Cluj-Napoca, Romania},
month = {September},
opturl = {http://dx.doi.org/},
isbn = {978-973-662-233-5},
issn = {},
optorganization = {},
publisher = {U.T.Press},
pdf = {iccp2006.pdf},
abstract = {Component based software development techniques are becoming
increasingly popular, as they improve the software development process
through component reuse. However component based development poses a
challenge to software verification: How can we assert the correctness
of a black-box component without having access to the internal logic
of its implementation? In this paper, we propose an approach to this
challenge by validating a component's communication history with
respect to a specification of its observable behaviour using runtime
verification techniques. For this purpose we present a simple
specification language for describing component behaviour in terms of
communication protocols, a language extension to support error
handling at the communication level, and a prototype tool to monitor
components and assert that they satisfy their protocol specification
at runtime. The prototype is implemented for Java components, supports
multithreaded access to the monitored components, and is demonstrated
on two examples.}
}
@inproceedings{KPS08tbr,
author = {Marcel Kyas and Cristian Prisacariu and Gerardo Schneider},
title = {Run-time Monitoring of Electronic Contracts},
booktitle = {{6th International Symposium on Automated Technology for Verification and Analysis (ATVA'08)}},
pages = {397--407},
volume = {5311},
series = {LNCS},
address = {Seoul, South Korea},
month = {October},
publisher = {Springer-Verlag},
year = {2008},
url = {http://dx.doi.org/10.1007/978-3-540-88387-6_34},
issn = {0302-9743},
isbn = {978-3-540-88386-9},
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 specification language that allows writing conditional
obligations, permissions and prohibitions.
We first give a trace semantics for CL which formalises that a trace fulfills a contract. We show how to
obtain, for a given contract, a linear-size
alternating Büchi automaton accepting exactly the traces
which fulfill the contract. This automaton is the basis for obtaining a
finite state machine which acts as a run-time monitor for CL contracts.},
pdf = {atva2008.pdf}
}
@inproceedings{OS08wos,
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)},
pages = {127--143},
series = {ENTCS},
volume = {253},
number = {1},
address = {York, UK},
year = {2009},
month = {March},
url = {http://dx.doi.org/10.1016/j.entcs.2009.09.032},
issn = {1571-0661},
isbn = {},
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 = {fesca09-wrappers.pdf}
}
@proceedings{OS09flacos,
title = {{Special Issue: Formal Languages and Analysis of Contract-Oriented Software (FLACOS'07)}},
year = {2009},
editor = {Olaf Owe and Gerardo Schneider},
volume = {78(5)},
number = {5},
series = {{Journal of Logic and Algebraic Programming}},
optaddress = {},
month = {May/June},
optorganization = {},
issn = {1567-8326},
isbn = {},
publisher = {Elsevier},
url = {http://dx.doi.org/10.1016/j.jlap.2009.02.012}
}
@proceedings{PS10flacos,
title = {{Special Issue: Formal Languages and Analysis of Contract-Oriented Software (FLACOS'08)}},
year = {2011},
editor = {Gordon Pace and Gerardo Schneider},
volume = {80(1)},
number = {1},
series = {{Journal of Logic and Algebraic Programming}},
optaddress = {},
month = {January},
optorganization = {},
issn = {1567-8326},
isbn = {},
publisher = {Elsevier},
url = {http://dx.doi.org/10.1016/j.jlap.2010.10.003}
}
@techreport{OSS07,
author = {Olaf Owe and Gerardo Schneider and Martin Steffen},
title = {Components, Objects, and Contracts},
institution = {Department of Informatics, University of Oslo},
year = {2007},
number = {363},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
isbn = {82-7368-321-4},
issn = {0806-3036},
month = {August},
pdf = {report-UiO-363.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.}
}
@inproceedings{OSS07coc,
author = {Olaf Owe and Gerardo Schneider and Martin Steffen},
title = {Components, Objects, and Contracts},
booktitle = {{6th Workshop on Specification And Verification of Component-Based Systems (SAVCBS'07)}},
optcrossref = {},
optkey = {},
pages = {95--98},
year = {2007},
opteditor = {},
series = {ACM Digital Library},
address = {Dubrovnik, Croatia},
month = {September},
optorganization = {},
optpublisher = {},
pdf = {savcbs2007.pdf},
url = {http://dx.doi.org/10.1145/1292316.1292328},
issn = {},
isbn = {978-1-59593-721-6},
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.}
}
@inproceedings{OST07tix,
author = {Olaf Owe and Gerardo Schneider and Arild Torjusen},
title = {{Towards integration of XML in the Creol object-oriented language}},
booktitle = {NIK'07 proceedings},
pages = {107--111},
year = {2007},
opteditor = {},
optvolume = {},
optnumber = {},
publisher = {Tapir Akademisk Forlag},
opturl = {http://dx.doi.org/},
issn = {},
isbn = {9788251922722},
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.},
pdf = {nik2007.pdf}
}
@techreport{OST07tr,
author = {Olaf Owe and Gerardo Schneider and Arild Torjusen},
title = {{Towards integration of XML in the Creol object-oriented language}},
institution = {Department of Informatics, University of Oslo},
year = {2007},
number = {365},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
isbn = {82-7368-323-0},
issn = {0806-3036},
month = {October},
pdf = {report-UiO-365.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.}
}
@techreport{PPS07TRmcc,
author = {Gordon Pace and Cristian Prisacariu and Gerardo Schneider},
title = {Model Checking Contracts --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 = {August},
pdf = {report-UiO-362.pdf},
issn = {0806-3036},
isbn = {},
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{PPS07mcc,
author = {Gordon Pace and Cristian Prisacariu and Gerardo Schneider},
title = {Model Checking Contracts --A Case Study},
booktitle = {{5th International Symposium on Automated Technology for Verification and Analysis (ATVA'07)}},
pages = {82--97},
year = {2007},
volume = {4762},
series = {LNCS},
address = {Tokyo, Japan},
month = {October},
publisher = {Springer-Verlag},
pdf = {atva2007.pdf},
url = {http://dx.doi.org/10.1007/978-3-540-75596-8_8},
issn = {0302-9743},
isbn = {978-3-540-75595-1},
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{PS04mcp,
author = {Gordon Pace and Gerardo Schneider},
title = {Model Checking Polygonal Differential Inclusions Using Invariance Kernels},
booktitle = {5th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'04)},
pages = {110--121},
year = {2003},
number = {2937},
series = {LNCS},
address = {Venice, Italy},
month = {December},
publisher = {Springer Verlag},
pdf = {vmcai2004.pdf},
url = {http://dx.doi.org/10.1007/978-3-540-24622-0_11},
issn = {0302-9743},
isbn = {978-3-540-20803-7},
abstract = {Polygonal hybrid systems are a subclass of planar hybrid automata
which can be represented by piecewise constant differential
inclusions. Here, we identify and compute an important object of
such systems' phase portrait, namely {\em invariance kernels}. An
\emph{invariant set} is a set of initial points of trajectories
which keep rotating in a cycle forever and the \emph{invariance
kernel} is the largest of such sets. We show that this kernel is a
non-convex polygon and we give a non-iterative algorithm for
computing the coordinates of its vertices and edges. Moreover, we
present a breadth-first search algorithm for solving the
reachability problem for such systems. Invariance kernels play an
important role in the algorithm.}
}
@inproceedings{PS06,
author = {Gordon Pace and Gerardo Schneider},
title = {Static Analysis for State-Space Reduction of Polygonal Hybrid Systems},
booktitle = {4th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'06)},
pages = {306--321},
year = {2006},
opteditor = {},
volume = {4202},
optnumber = {},
series = {LNCS},
address = {Paris, France},
month = {September},
publisher = {Springer-Verlag},
pdf = {formats2006.pdf},
url = {http://dx.doi.org/10.1007/11867340_22},
issn = {0302-9743},
isbn = {978-3-540-45026-9},
abstract = {Polygonal hybrid systems (SPDI) are a subclass of planar hybrid automata which can be represented by piecewise constant differential
inclusions. The reachability problem as well as the computation of
certain objects of the phase portrait, namely the viability,
controllability and invariance kernels, for such systems is
decidable. In this paper we show how to compute another object of an
SPDI phase portrait, namely semi-separatrix curves and show how the
phase portrait can be used for reducing the state-space for
optimizing the reachability analysis.}
}
@inproceedings{PS06cap,
author = {Gordon J. Pace and Gerardo Schneider},
title = {A Compositional Algorithm for Parallel Model Checking of Polygonal Hybrid Systems},
booktitle = {3rd International Colloquium on Theoretical Aspects of Computing (ICTAC'06)},
pages = {168--182},
year = {2006},
opteditor = {},
volume = {4281},
optnumber = {},
series = {LNCS},
address = {Tunis, Tunisia},
month = {November},
publisher = {Springer-Verlag},
pdf = {ictac2006.pdf},
url = {http://dx.doi.org/10.1007/11921240_12},
issn = {0302-9743},
isbn = {3-540-48815-4},
abstract = {The reachability problem as well as the computation of the phase portrait for
polygonal hybrid systems (SPDI) has been shown to be decidable. The existing
reachability algorithm is based on the exploitation of topological properties
of the plane which are used to accelerate certain kind of cycles. The exponential
nature of the algorithm makes the analysis of large systems generally unfeasible.
In this paper we present a compositional parallel algorithm for
reachability analysis of SPDIs. The parallelization is based on the qualitative information obtained from the phase portrait of an SPDI, in particular the
controllability kernel.}
}
@booklet{PS06iph,
title = {Improving Polygonal Hybrid Systems Reachability Analysis through the use of the Phase Portrait},
author = {Gordon Pace and Gerardo Schneider},
howpublished = {CSAW'06},
address = {Malta},
optmonth = {},
year = {2006},
pdf = {csaw2006.pdf}
}
@techreport{PS06sas,
author = {Gordon Pace and Gerardo Schneider},
title = {Static Analysis of {SPDI}s for State-Space Reduction},
institution = {Department of Informatics, University of Oslo},
year = {2006},
number = {336},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
month = {April},
pdf = {report-UiO-336.pdf},
isbn = {82-7368-291-9},
issn = {0806-3036},
abstract = {Polygonal hybrid systems (SPDI) are a subclass of planar hybrid automata which can be represented by piecewise constant differential
inclusions. The reachability problem as well as the computation of
certain objects of the phase portrait, namely the viability,
controllability and invariance kernels, for such systems is
decidable. In this paper we show how to compute another object of an
SPDI phase portrait, namely semi-separatrix curves and show how the
phase portrait can be used for reducing the state-space for
optimizing the reachability analysis.}
}
@inproceedings{PS07cvp,
author = {Gordon Pace and Gerardo Schneider},
title = {Computation and Visualisation of Phase Portraits of Polygonal Hybrid Systems --{Tool Paper}},
booktitle = {{14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08)}},
month = {March},
year = {2008},
volume = {4963},
series = {LNCS},
address = {Budapest, Hungary},
publisher = {Springer-Verlag},
pages = {341--345},
url = {http://dx.doi.org/10.1007/978-3-540-78800-3_25},
issn = {0302-9743},
isbn = {978-3-540-78799-0},
abstract = {Hybrid systems combining discrete and continuous dynamics arise as mathematical models of various artificial and natural systems, and as an approximation to complex continuous systems. We present the tool SPeeDI+, that extends SPeeDI (a tool that implements a reachability algorithm for polygonal hybrid systems) with the computation of viability, controllability and invariance kernels.},
pdf = {tacas2008-tool.pdf}
}
@inproceedings{PS07fle,
title = {A Formal Language for Electronic Contracts},
author = {Prisacariu, Cristian and Schneider, Gerardo},
year = {2007},
booktitle = {9th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS'07)},
volume = {4468},
pages = {174--189},
series = {LNCS},
month = {June},
publisher = {Springer},
address = {Paphos, Cyprus},
url = {http://dx.doi.org/10.1007/978-3-540-72952-5_11},
issn = {0302-9743},
isbn = {978-3-540-72919-8},
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 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.},
pdf = {fmoods2007.pdf}
}
@techreport{PS07tfd,
author = {Cristian Prisacariu and Gerardo Schneider},
title = {Towards a Formal Definition of Electronic Contracts},
institution = {Department of Informatics, University of Oslo},
year = {2007},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
month = {January},
number = {348},
isbn = {82-7368-305-2},
issn = {0806-3036},
pdf = {report-UiO-348.pdf},
abstract = {In this technical report we discuss the main problems arising when defining a language for contracts. We propose a formal language for writing electronic contracts, based on the deontic notions of obligation, prohibition, and permission. 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, and 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 that it avoids most of the classical paradoxes of deontic logic. We finally show its applicability on a contract example.}
}
@booklet{PS07tmc,
title = {Towards Model Checking Contracts},
author = {Cristian Prisacariu and Gerardo Schneider},
howpublished = {{NWPT'07/FLACOS'07 Workshop Proceedings}},
pages = {104-106},
address = {Oslo, Norway},
month = {October 9--10},
year = {2007},
note = {Extended Abstract},
pdf = {flacos2007.pdf}
}
@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},
issn = {0806-3036},
isbn = {82-7368-319-2},
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 = {report-UiO-361.pdf},
note = {Updated March 2008}
}
@techreport{PS08TRrgs,
author = {Gordon Pace and Gerardo Schneider},
title = {{Relaxing Goodness is Still Good for SPDIs}},
month = {February},
institution = {Department of Informatics, University of Oslo},
year = {2008},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
month = {January},
number = {372},
isbn = {82-7368-331-1},
issn = {0806-3036},
pdf = {report-UiO-372.pdf},
abstract = {Polygonal hybrid systems (SPDIs) are planar hybrid systems, whose dynamics are defined in terms of constant differential inclusions, one for each of a number of polygonal regions partitioning the plane. The reachability problem for SPDIs is known to be decidable, but depends on the \emph{goodness} assumption --- which states that the dynamics do not allow a trajectory to both enter and leave a region through the same edge. In this paper we extend the decidability result to {\em generalised SPDIs} (GSPDI), SPDIs not satisfying the goodness property, and give an algorithmic solution to decide reachability of such systems.}
}
@inproceedings{PS08csf,
author = {Gordon J. Pace and Gerardo Schneider},
title = {Challenges in the Specification of Full Contracts},
booktitle = {{Integrated Formal Methods (iFM'09)}},
pages = {292--306},
volume = {5423},
series = {LNCS},
address = {D\"useldorf, Germany},
year = {2009},
month = {February},
pdf = {ifm2009.pdf},
url = {http://dx.doi.org/10.1007/978-3-642-00255-7_20},
issn = {0302-9743},
isbn = {978-3-642-00254-0},
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.}
}
@techreport{PS08flacos,
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},
isbn = {82-7368-337-0},
issn = {0806-3036},
month = {October},
note = {Editors},
pdf = {report-UiO-377.pdf}
}
@inproceedings{PS08rgs,
author = {Gordon J. Pace and Gerardo Schneider},
title = {Relaxing Goodness is Still Good},
booktitle = {{5th International Colloquium on Theoretical Aspects of Computing (ICTAC'08)}},
pages = {274--289},
opteditor = {J.S.Fitzgerald and A.E. Haxhausen and H. Yenigun},
volume = {5160},
series = {LNCS},
address = {Istanbul, Turkey},
month = {September},
year = {2008},
url = {http://dx.doi.org/10.1007/978-3-540-85762-4_19},
issn = {0302-9743},
isbn = {978-3-540-85761-7},
abstract = {Polygonal hybrid systems (SPDIs) are planar hybrid systems, whose dynamics are defined in terms of constant differential inclusions, one for each of a number of polygonal regions partitioning the plane. The reachability problem for SPDIs is known to be decidable, but depends on the \emph{goodness} assumption --- which states that the dynamics do not allow a trajectory to both enter and leave a region through the same edge. In this paper we extend the decidability result to {\em generalised SPDIs} (GSPDI), SPDIs not satisfying the goodness property, and give an algorithmic solution to decide reachability of such systems.},
pdf = {ictac2008.pdf}
}
@techreport{PS08tr371,
title = {{CL: A Logic for Reasoning about Legal Contracts ---Semantics}},
author = {Cristian Prisacariu and Gerardo Schneider},
publisher = {Department of Informatics, University of Oslo},
address = {Oslo, Norway},
pages = {68},
number = {371},
year = 2008,
month = {February},
issn = {0806-3036},
isbn = {82-7368-330-3},
abstract = {The work reported here is concerned with the definition of a logic (which we call CL) for reasoning about legal contracts. The report presents the syntax of the logic and the associated semantics. There are two semantics presented: one is defined with respect to linear structures (i.e. traces of actions) and is intended for run-time monitoring of executions of contracts; the second semantics is given over branching structures (i.e. Kripke-like structures) and is intended for reasoning about contracts in a static manner (i.e. model-checking and theorem proving). In the first part of the report we present the theoretical results underlying the branching semantics. It presents an algebra of actions and restates some of previous results presented in another report, as well as new results useful for the definition of the branching semantics and for the proofs. The rest of the report is concerned with the definition of the two semantics. Moreover, several (non-standard) desired properties of the logic are proven.},
pdf = {report-UiO-371.pdf}
}
@inproceedings{PS09asl,
author = {Cristian Prisacariu and Gerardo Schneider},
title = {Abstract Specification of Legal Contracts (Research Abstract)},
booktitle = {12th International Conference on Artificial Intelligence and Law (ICAIL'09)},
pages = {218--219},
year = {2009},
opteditor = {},
optvolume = {},
address = {Barcelona, Spain},
month = {June},
publisher = {ACM},
url = {http://dx.doi.org/10.1145/1568234.1568262},
issn = {},
isbn = {978-1-60558-597-0},
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 electronic contracts, and as an abstract language for legal contracts. CL combines the legal notions of obligation, permission, and prohibition from deontic logic with the action modality of propositional dynamic logic. 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 discussion of the choices made for designing CL, both syntactically and semantically.},
pdf = {icail09.pdf}
}
@inproceedings{PS09cl,
author = {Cristian Prisacariu and Gerardo Schneider},
title = {{CL: An Action-based Logic for Reasoning about Contracts}},
booktitle = {16th Workshop on Logic, Language, Information and Computation (WOLLIC'09)},
pages = {335--349},
year = {2009},
opteditor = {},
volume = {5514},
series = {LNCS},
address = {Tokyo, Japan},
month = {June},
publisher = {Springer},
url = {http://dx.doi.org/10.1007/978-3-642-02261-6_27},
issn = {0302-9743},
isbn = {978-3-642-02260-9},
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.},
pdf = {wollic09.pdf}
}
@booklet{SA96ill,
title = {Introduction to linear logic},
author = {Gerardo Schneider and Rafael Accorsi},
howpublished = {Primeiro Workshop sobre M\'etodos Formais e Qualidade de Software},
address = {Porto alegre, Brazil},
month = {July},
year = {1996},
pages = {15--42},
note = {(In Portuguese)}
}
@booklet{SR96spc,
title = {Sequential and parallel computation strategies on coherence spaces},
author = {Gerardo Schneider and Ant\^onio C. da Rocha Costa},
howpublished = {CLEI'96},
address = {Bogot\'a, Colombia},
month = {June},
year = {1996},
pages = {276--287}
}
@booklet{SR97cse,
title = {Coherence space as event structure and concrete data structure},
author = {Gerardo Schneider and Ant\^onio C. da Rocha Costa},
howpublished = {XXIV SEMISH},
address = {Brasilia, Brazil},
month = {August},
year = {1997},
pages = {423--434}
}
@booklet{ST95fpt,
title = {Fixed point theory in Computer Science},
author = {Gerardo Schneider and Laira V. Toscani},
howpublished = {Anais do CNMAC},
address = {Curitiba, Brazil},
month = {August},
year = {1995},
pages = {150--154},
note = {(Extended abstract, in Portuguese)}
}
@inproceedings{SX98tfs,
author = {Gerardo Schneider and Xu Qiwen},
title = {Towards a Formal Semantics of Verilog using Duration Calculus},
booktitle = {5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'98)},
pages = {282--293},
year = {1998},
opteditor = {Anders P. Ravn and Hans Rischel},
number = {1486},
series = {LNCS},
address = {Lyngby, Denmark},
month = {September},
publisher = {Springer Verlag},
pdf = {ftrtft98.pdf},
url = {http://dx.doi.org/10.1007/BFb0055355},
issn = {0302-9743},
isbn = {978-3-540-65003-4},
abstract = {We formalise the semantics of $V^-$, a simple version of Verilog
hardware description language using an extension of Duration Calculus.
The language is simple enough for experimenting formalisation, but
contains sufficient features
for being practically relevant. $V^-$ programs can exhibit a rich
variety of computations, and it is therefore necessary to extend
Duration Calculus with several features, including Weakly Monotonic Time,
infinite intervals and fixed point operators. The semantics is compositional
and can be used as the formal basis of a formal theory of Verilog.}
}
@techreport{SX98tos,
author = {Gerardo Schneider and Xu Qiwen},
title = {{Towards an Operational Semantics of Verilog}},
institution = {UNU/IIST},
year = {1998},
number = {147},
address = {P.O.Box 3058, Macau},
month = {October},
ps = {report147.ps.gz},
issn = {},
isbn = {},
abstract = {We give an operational semantics of $V^-$, a simple version of Verilog
hardware description language..
The language is simple enough for experimenting formalisation, but
contains sufficient features
for being practically relevant. $V^-$ programs can exhibit a rich
variety of computations that justifies the introduction of labels in the transition relation to represent the execution of components, time passing and passive transitions. The semantics is compositional
and can be used as the formal basis of a formal theory of Verilog.}
}
@techreport{giambiagi98avs,
author = {Pablo Giambiagi and Gerardo Schneider},
title = {{A Verilog specification of STARI}},
institution = {UNU/IIST},
year = {1998},
address = {P.O.Box 3058, Macau},
month = {February},
ps = {stari.ps.gz},
issn = {},
isbn = {},
abstract = {Verilog is a Hardware Description Language used for the design and
description of hardware in a behavioral and structural way. It has some interesting features like concurrency, synchronism,
shared variables, non-blocking assignments (scheduled assignments),
timing controls, infinite computations, zero-time computations, etc.,
that makes it an interesting language to study. This report explains
some features of Verilog in an informal way through small examples and
presents the Verilog code of STARI as a main application.}
}
@inproceedings{lafferriere00psr,
author = {Gerardo Lafferriere and George J. Pappas and Gerardo
Schneider and Sergio Yovine},
title = {Parameter Synthesis in Robot Motion Planning Using
Symbolic Reachability Computation},
booktitle = {Proceedings of 8th IEEE Mediterranean Conference
on Control and Automation},
pages = {},
address = {Rio, Greece},
month = {July},
year = {2000},
pdf = {med2000.pdf},
opturl = {http://dx.doi.org/},
issn = {},
isbn = {},
abstract = {A well known problem in robotics is the motion planning
problem in the presence of static obstacles. The trajectory of
the robot must satisfy a linear differential equation as
well as possbile input and state constraints. In this
paper, we explore the use of symbolic reachability algorithms
to decide whether the motion planning problem is feasible
or not. In the case where it is feasible, it computes a feasible
nominal input profile satisfying all system constraints. Our algorithm
is based on quantifier elimination techniques in the ordered field of
the reals, which have been recently applied to compute the reachable
space for classes of linear hybrid systems.}
}
@phdthesis{schneider02,
author = {Gerardo Schneider},
title = {Algorithmic Analysis of Polygonal Hybrid Systems},
school = {VERIMAG -- UJF},
year = {2002},
address = {Grenoble, France},
month = {July},
pdf = {PhDthesis.pdf},
issn = {},
isbn = {},
abstract = {A {\em polygonal differential inclusion system} (SPDI) is a non-deterministic planar hybrid system which can be represented by piecewise constant differential inclusions. In this thesis we are concerned with several theoretical and practical questions related to SPDIs such as reachability analysis and phase portrait construction.
First we show that the reachability question for SPDIs is indeed decidable. Our procedure is not based on the computation of the reach-set but rather on the computation of the limit of individual trajectories. A key idea is the use of edge-to-edge one-dimensional affine Poincar\'e maps, the fix-points of which are easily computed. By taking advantage of this information, cycles can be {\em accelerated} in most cases.
The above reachability algorithm has been implemented in a tool called SPeeDI.
We next build the phase portrait of such systems. In particular, we identify the \emph{viability} kernels of simple cycles. Such kernels are the set of starting points of trajectories that can keep rotating in the cycles forever. We also introduce the notion of \emph{controllability} kernel of simple cycles as the set of points such that any two points of the set are reachable from each other {\em via} trajectories that remain on the set. We give non-iterative algorithms to compute both kernels. We obtain the SPDI phase portrait computing all the viability and controllability kernels.
We finally study the decidability of the reachability problem for other 2-dimensional hybrid systems. We introduce {\em hierarchical piecewise constant derivative systems} (HPCDs) and {\em 2-dimensional manifolds with piecewise constant derivative systems}. We show that the reachability problem for the above two classes of systems is as hard as the reachability problem for {\em piecewise affine maps} that is known to be an open problem. We also show that the reachability question for slight extensions of HPCDs are undecidable.}
}
@booklet{schneider03cik,
title = {Computing invariance kernels of polygonal hybrid systems},
author = {Gerardo Schneider},
howpublished = {NWPT'2003},
address = {Turku, Finland},
month = {October 29--31},
year = {2003},
note = {Extended Abstract},
ps = {nwpt03_ik.ps.gz}
}
@techreport{schneider03ikp,
author = {Gerardo Schneider},
title = {Invariance Kernels of Polygonal Differential Inclusions},
institution = {Department of Information Technology, Uppsala University},
year = {2003},
number = {2003-042},
month = {August},
ps = {tec_rep_2003-042.ps.gz},
issn = {},
isbn = {},
abstract = {This is the technical report corresponding to the journal paper "Computing invariance kernels of polygonal hybrid systems".}
}
@techreport{schneider04cba,
author = {Gerardo Schneider},
title = {A constraint-based algorithm for analysing memory usage on Java cards},
institution = {INRIA},
year = {2004},
number = {RR-5440},
month = {December},
ps = {RR-5440.ps.gz},
issn = {},
isbn = {},
abstract = {We address in this paper the problem of statically determining whether a JavaCard applet may produce a memory overflow because of the dynamic instantiation of classes inside cycles. We provide a constraint-based algorithm which determines potential loops and (mutually) recursive methods. The algorithm operates on the byte-code of an applet. It is written as a set of rules --one for each byte-code instruction-- which allows a compositional reasoning and it comprises both inter- and intra-procedural analysis. We aimed at an algorithm suitable to be fed into the proof assistant Coq in order to extract a certified memory usage analyser. We prove termination of the algorithm as well as its soundness and completeness with respect to an abstraction of the operational semantics of the language.}
}
@booklet{schneider04mue,
title = {Memory usage estimation for Java cards},
author = {Gerardo Schneider},
howpublished = {NWPT'2004},
address = {Uppsala, Sweden},
month = {October 06--08},
year = {2004},
note = {Extended Abstract},
ps = {nwpt04.ps.gz}
}
@article{schneider04njc,
author = {Gerardo Schneider},
title = {Computing Invariance Kernels of Polygonal Hybrid Systems},
journal = {Nordic Journal of Computing},
year = {2004},
volume = {11},
number = {2},
pages = {194--210},
pdf = {njc.pdf},
opturl = {http://dx.doi.org/},
issn = {1236-6064},
abstract = {Polygonal hybrid systems are a subclass of planar hybrid automata
which can be represented by piecewise constant differential
inclusions. One way of analysing such systems (and hybrid systems in general) is through the study of their phase portrait, which characterise the systems' qualitative behaviour.
In this paper we identify and compute an important object of polygonal hybrid systems' phase portrait, namely {\em invariance kernels}. An \emph{invariant set} is a set of points such that any trajectory starting in such point keep necessarily rotating in the set forever and the \emph{invariance kernel} is the largest of such sets. We show that this kernel is a non-convex polygon and we give a non-iterative algorithm for computing the coordinates of its vertexes and edges. Moreover, we show some properties of such systems' simple cycles.
}
}
@techreport{schneider05tcp,
author = {Gerardo Schneider},
title = {Towards Computing Phase Portrait Objects of Polygonal Hybrid Systems on Surfaces},
institution = {Department of Informatics, University of Oslo},
year = {2005},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
month = {March},
number = {331},
isbn = {82-7368-286-2},
issn = {0806-3036},
pdf = {report-UiO-331.pdf},
abstract = {Polygonal hybrid systems (SPDIs) are a subclass of hybrid systems whose dynamics is defined by constant differential inclusions. We can define SPDIs on surfaces, obtaining a new class of hybrid systems.
In this paper we define and compute various phase portrait objects of this new class: invariance, controllability and viability kernels and separatrix sets.}
}
@techreport{schneider07drp,
author = {Gerardo Schneider},
title = {On the Decidability of the Reachability Problem for {GSPDIs}},
institution = {Department of Informatics, University of Oslo},
year = {2007},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
month = {June},
number = {359},
isbn = {82-7368-317-6},
issn = {0806-3036},
pdf = {report-UiO-359.pdf},
abstract = {Polygonal hybrid systems (SPDIs) are a subclass of hybrid systems whose dynamics is defined by constant differential inclusions, for which the reachability problem is decidable. The decidability result is based, among other things, on the fact that a trajectory cannot enter and leave a given region through the same edge. An SPDI satisfying the above restriction is said to have the {\em goodness} property. In a previous work we have given an incomplete proof of decidability of reachability for SPDIs when relaxing goodness. In this work we give a counter-example to such proof and we give an algorithm for semi-deciding reachability of such class of systems.}
}
@inproceedings{schneider08rag,
author = {Gerardo Schneider},
title = {Reachability Analysis of {Generalized Polygonal Hybrid Systems}},
booktitle = {23rd Annual ACM Symposium on Applied Computing --Software Verification track (SAC-SV'08)},
pages = {327--332},
address = {Fortaleza, Brazil},
month = {March},
year = {2008},
url = {http://dx.doi.org/10.1145/1363686.1363773},
isbn = {978-1-59593-753-7},
publisher = {ACM},
abstract = {A polygonal hybrid system (SPDIs) is a planar hybrid system, whose dynamics is defined by constant differential inclusions, for which the reachability problem is decidable. The decidability result is based, among other things, on the fact that a trajectory cannot enter and leave a given region through the same edge (the so-called {\it goodness} assumption). SPDIs without such an assumption are called Generalized SPDIs (GSPDIs).
In this paper we show that it is not possible to reduce GSPDI reachability to SPDI reachability. Furthermore, we show that the reachability algorithm for SPDIs can be used to semi-decide GSPDI reachability, for which we give a sound algorithm.},
pdf = {sac-sv2008.pdf}
}
@techreport{schneider92uia,
author = {Gerardo Schneider},
title = {{Using induction for algorithm design}},
institution = {{Dissertation for Engineering Degree. Facultad Regional Concepci\'on del Uruguay - UTN}},
year = {1992},
address = {Concepci\'on del Uruguay, Argentina},
month = {December},
pages = {91},
note = {(In Spanish)}
}
@techreport{schneider94asl,
author = {Gerardo Schneider},
title = {{An algebraic specification language}},
institution = {CPGCC da UFRGS},
year = {1994},
address = {Porto Alegre, Brazil},
month = {July},
pages = {44},
note = {(In Portuguese)}
}
@techreport{schneider95fpt,
author = {Gerardo Schneider},
title = {{Fixed point theory in Computer Science}},
institution = {CPGCC da UFRGS},
year = {1995},
address = {Porto Alegre, Brazil},
month = {January},
pages = {68},
note = {(In Portuguese)}
}
@mastersthesis{schneider96,
author = {Gerardo Schneider},
title = {Sequential and Parallel Computation Strategies on Coherence Spaces},
school = {CPGCC -- UFRGS},
year = {1996},
address = {Porto Alegre, Brazil},
month = {March},
note = {(In Portuguese)},
ps = {tesis.ps.gz},
pages = {144}
}
@techreport{schneider98tfs,
author = {Gerardo Schneider and Xu Qiwen},
title = {{Towards a Formal Semantics of Verilog using Duration Calculus}},
institution = {UNU/IIST},
year = {1998},
number = {133},
address = {P.O.Box 3058, Macau},
month = {February},
ps = {report133.ps.gz},
issn = {},
isbn = {},
abstract = {Verilog is a Hardware Description Language used for the design and
description of hardware in a behavioral and structural way. The meaning of a Verilog program is given by a
simulation semantics, which is based on events and lack the necessary
formality. Clearly it would be desirable to have a logical formal semantics to
reason about properties of Verilog programs and to prove, among other things, the
equivalence between programs (specification and implementation). Verilog has some interesting features like concurrency, synchronism,
shared variables, non-blocking assignments (scheduled assignments),
timing controls, infinite computations, zero-time computations, etc.,
that makes it an interesting language to study. WDC (Duration Calculus
with Weakly Monotonic Time), introduced by Pandya and Dang,
seems to provide an appropriate semantical framework for formalising
languages with zero-time delays and computations. We introduce a fixed point
operator and infinite intervals in WDC obtaining MWDCI. We use MWDCI to give
a compositional abstract semantics to the $V^-$ subset of Verilog and
in particular the fixed point operator is used to give semantics to the loop statements modelling infinite computation taking zero time
(infinite in the discrete time) as well as infinite computation in the
macro-time. We prove
some results (at the semantical level) about the fixed point operator.}
}
This file was generated by bibtex2html 1.92.