@inproceedings{LAPS23ttp,
author = {David Lidell and Shaun Azzopardi and Nir Piterman and Gerardo Schneider},
title = {ppLTLTT: Temporal Testing for Pure-Past Linear Temporal Logic Formulae},
booktitle = {21st International Symposium on Automated Technology for Verification and Analysis (ATVA'23)},
year = {2023},
opteditor = {{\'{E}}tienne Andr{\'{e}} and Jun Sun},
volume = {14216},
optseries = {},
pages = {276-287},
optmonth = {24-27 October},
optaddress = {Singapore},
doi = {10.1007/978-3-031-45332-8\_15},
publisher = {LNCS},
abstract = {This paper presents ppLTLTT, a tool for translating pure-past linear temporal logic formulae into temporal testers in the form of automata. We show how ppLTLTT can be used to easily extend existing LTL-based tools, such as LTL-to-automata translators and reactive synthesis tools, to support a richer input language. Namely, with ppLTLTT, tools that accept LTL input are also made to handle pure-past LTL as atomic formulae. While the addition of past operators does not increase the expressive power of LTL, it opens up the possibility of writing more intuitive and succinct specifications. We illustrate this intended use of ppLTLTT for Slugs, Strix, and Spot ’s command line tool LTL2TGBA by describing three corresponding wrapper tools pSlugs, pStrix, and pLTL2TGBA, that all leverage ppLTLTT. All three wrapper tools are designed to seamlessly fit this paradigm, by staying as close to the respective syntax of each underlying tool as possible.}
}
@inproceedings{KASL23sav,
author = {Karam Kharraz and Shaun Azzopardi and Gerardo Schneider and Martin Leucker},
title = {Synchronous Agents, Verification, and Blame -- A Deontic View},
booktitle = {20th International Colloquium on Theoretical Aspects of Computing (ICTAC'23)},
year = {2023},
opteditor = {Erika {\'{A}}brah{\'{a}}m and Clemens Dubslaff and Silvia Lizeth Tapia Tarifa},
volume = {14446},
pages = {332--350},
series = {LNCS},
optmonth = {4-8 December},
optaddress = {Lima, Peru},
doi = {10.1007/978-3-031-47963-2\_20},
publisher = {Springer},
abstract = {A question we can ask of multi-agent systems is whether the agents’ collective interaction satisfies particular goals or specifications, which can be either individual or collective. When a collaborative goal is not reached, or a specification is violated, a pertinent question is whether any agent is to blame. This paper considers a two-agent synchronous setting and a formal language to specify when agents’ collaboration is required. We take a deontic approach and use obligations, permissions, and prohibitions to capture notions of non-interference between agents. We also handle reparations, allowing violations to be corrected or compensated. We give trace semantics to our logic, and use it to define blame assignment for violations. We give an automaton construction for the logic, which we use as the base for model checking and blame analysis. We also further provide quantitative semantics that is able to compare different interactions in terms of the required reparations.}
}
@inproceedings{EAHS23csc,
author = {Mojtaba Eshghie and Wolfgang Ahrendt and Thomas Hildebrandt and Gerardo Schneider},
title = {Capturing Smart Contract Design with DCR Graphs},
booktitle = {21st International Conference on Software Engineering and Formal Methods (SEFM'23)},
year = {2023},
opteditor = {Carla Ferreira and Tim A. C. Willemse},
volume = {14323},
pages = {106--125},
series = {LNCS},
optmonth = {6-10 November},
optaddress = {Eindhoven, The Netherlands},
doi = {10.1007/978-3-031-47115-5\_7},
publisher = {Springer},
abstract = {Smart contracts manage blockchain assets and embody business processes. However, mainstream smart contract programming languages such as Solidity lack explicit notions of roles, action dependencies, and time. Instead, these concepts are implemented in program code. This makes it very hard to design and analyze smart contracts. We argue that DCR graphs are a suitable formalization tool for smart contracts because they explicitly and visually capture the mentioned features. We utilize this expressiveness to show that many common high-level design patterns representing the underlying business processes in smart-contract applications can be naturally modeled this way. Applying these patterns shows that DCR graphs facilitate the development and analysis of correct and reliable smart contracts by providing a clear and easy-to-understand specification.}
}
@article{AJPS23abe,
author = {Hamed Arshad and
Christian Johansen and
Pablo Picazo{-}Sanchez and
Gerardo Schneider},
title = {Attribute-Based Encryption with Enforceable Obligations},
journal = {Journal of Cryptographic Engineering},
year = {2023},
volume = {13},
number = {3},
pages = {343--371},
abstract = {Attribute-Based Encryption (ABE) is a cryptographic mechanism that provides fine-grained access control to encrypted data, which can thus be stored in, e.g., public clouds. However, ABE schemes lack the notion of obligations, which is common in Attribute-Based Access Control systems such as eXtensible Access Control Markup Language and Usage Control. Obligations are used to define and enforce extra constraints that happen before approving or denying an access request. In this paper, we propose Attribute-Based Encryption with enforceable OBligations (OB-ABE), a system for extending any classical ABE with enforceable obligations. Our system architecture has as core component trusted hardware enclaves, implemented with Intel Software Guard Extensions (SGX), used for enforcing obligations. We employ ProVerif to formally model OB-ABE and verify its main property called ``enforceable obligations’’, i.e., if a message is encrypted along with an obligation, then the message can be decrypted only after enforcing the attached obligation. OB-ABE has two more properties: (i) OB-ABE is a ``conservative extension’’ of the underlying ABE scheme, preserving its security properties; (ii) OB-ABE is ``backward compatible’’ in the sense that any ciphertext produced by an ABE scheme can be decrypted by its extended OB-ABE version, and moreover, a ciphertext produced by an OB-ABE scheme can be decrypted by its underlying ABE scheme provided that the ciphertext does not have obligations attached.
We also implement in C using Intel SGX a prototype of an OB-ABE extending the well-known Ciphertext-Policy ABE.},
pdf = {JCE2023.pdf},
doi = {10.1007/s13389-023-00317-1}
}
@inproceedings{APS22rvm,
author = {Shaun Azzopardi and
Nir Piterman and
Gerardo Schneider},
opteditor = {Tiziana Margaria and Bernhard Steffen},
title = {Runtime Verification Meets Controller Synthesis},
booktitle = {11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles (ISoLA 2022), Proceedings, Part {I}},
address = {Rhodes, Greece},
series = {LNCS},
volume = {13701},
pages = {382--396},
publisher = {Springer},
year = {2022},
url = {https://doi.org/10.1007/978-3-031-19849-6\_22},
doi = {10.1007/978-3-031-19849-6\_22}
}
@article{PSS22ace,
author = {Pablo Picazo{-}Sanchez and
Lara Ortiz{-}Martin and
Gerardo Schneider and
Andrei Sabelfeld},
title = {Are chrome extensions compliant with the spirit of least privilege?},
journal = {International Journal of Information Security},
volume = {21},
number = {6},
pages = {1283--1297},
year = {2022},
url = {https://doi.org/10.1007/s10207-022-00610-w},
doi = {10.1007/s10207-022-00610-w},
abstract = {Extensions are small applications installed by users and enrich the user experience of browsing the Internet. Browsers expose a set of restricted APIs to extensions. To be used, extensions need to list the permissions associated with these APIs in a mandatory extension file named manifest. In particular, Chrome’s permission ecosystem was designed in the spirit of the least privilege. Yet, this paper demonstrates that 39.8\% of the analyzed extensions provided by the official Web Store are compliant with the spirit of least privilege. Also, we develop: (1) a browser extension to make aware regular users of the permissions the extensions they install; (2) a web app where extensions developers can check whether their extensions are compliant with the spirit of the least privileged; and (3) a set of scripts that can be part of the vendors’ acceptance criteria such that when developers upload their extensions to the official repositories, the scripts automatically analyze the extensions and generate a report about the permissions and the usage.},
pdf = {}
}
@inproceedings{ATS+22pap,
author = {Hanaa Alshareef and
Katja Tuma and
Sandro Stucki and
Gerardo Schneider and
Riccardo Scandariato},
title = {Precise Analysis of Purpose Limitation in Data Flow Diagrams},
booktitle = {{ARES} 2022: The 17th International Conference on Availability, Reliability and Security},
optaddress = {Vienna,Austria, Aug 23-26},
pages = {17:1--17:11},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3538969.3539010},
doi = {10.1145/3538969.3539010},
abstract = {Data Flow Diagrams (DFDs) are primarily used for modelling functional properties of a system. In recent work, it was shown that DFDs can be used to also model non-functional properties, such as security and privacy properties, if they are annotated with appropriate security- and privacy-related information. An important privacy principle one may wish to model in this way is purpose limitation. But previous work on privacy-aware DFDs (PA-DFDs) considers purpose limitation only superficially, without explaining how the purpose of DFD activators and flows ought to be specified, checked or inferred. In this paper, we define a rigorous formal framework for (1) annotating DFDs with purpose labels and privacy signatures, (2) checking the consistency of labels and signatures, and (3) inferring labels from signatures. We implement our theoretical framework in a proof-of concept tool consisting of a domain-specific language (DSL) for specifying privacy signatures and algorithms for checking and inferring purpose labels from such signatures. Finally, we evaluate our framework and tool through a case study based on a DFD from the privacy literature.},
pdf = {}
}
@inproceedings{GZS+22amt,
author = {Felipe Gorostiaga and
Sebasti{\'{a}}n Zudaire and
C{\'{e}}sar S{\'{a}}nchez and
Gerardo Schneider and
Sebasti{\'{a}}n Uchitel},
opteditor = {Tiziana Margaria and
Bernhard Steffen},
title = {Assumption Monitoring of Temporal Task Planning Using Stream Runtime Verification},
booktitle = {11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'22),
Rhodes, Greece, October 22-30, 2022, Proceedings, Part {I}},
optaddress = {Rhodes, Greece, Oct 22-30},
series = {Lecture Notes in Computer Science},
volume = {13701},
pages = {397--414},
publisher = {Springer},
year = {2022},
url = {https://doi.org/10.1007/978-3-031-19849-6\_23},
doi = {10.1007/978-3-031-19849-6\_23},
abstract = {Temporal task planning uses formal techniques such as reactive synthesis to guarantee that a robot will succeed in its mission. This technique requires certain explicit and implicit assumptions and simplifications about the operating environment of the robot, including its sensors and capabilities. A robot executing a plan can produce a silent mission failure, where the user may believe that the mission goals were achieved when instead the assumptions were violated at runtime. This entails that mitigation and remediation opportunities are missed. Monitoring at runtime can detect complex assumption violations and identify silent failures, but such monitoring requires the ability to describe and detect sophisticated temporal properties together with quantitative and complex data. Additional challenges include (1) ensuring the correctness of the monitors and a correct interplay between the planning execution and the monitors, and (2) that monitors run under constrained environments in terms of resources. In this paper we propose a solution based on stream runtime verification, which offers a high-level declarative language to describe sophisticated monitors together with guarantees on the execution time and memory usage. We show how monitors can be combined with temporal planning not only to monitor assumptions but also to support mitigation and remediation in UAV missions. We demonstrate our approach both in real and simulated flights for some typical mission scenarios.},
pdf = {}
}
@inproceedings{CPS22abf,
author = {Stefan Chircop and
Gordon J. Pace and
Gerardo Schneider},
opteditor = {Enrico Francesconi and
Georg Borges and
Christoph Sorge},
title = {An Automata-Based Formalism for Normative Documents with Real-Time},
booktitle = {Fifth International Conference on Legal Knowledge and Information Systems - {JURIX}'22},
optaddress = {Saarbr{\"{u}}cken, Germany, 14-16 December 2022},
series = {Frontiers in Artificial Intelligence and Applications},
volume = {362},
pages = {158--163},
publisher = {{IOS} Press},
year = {2022},
url = {https://doi.org/10.3233/FAIA220460},
doi = {10.3233/FAIA220460},
abstract = {Deontic logics have long been the tool of choice for the formal analysis of normative texts. While various such logics have been proposed many deal with time in a qualitative sense, i.e., reason about the ordering but not timing of events, it was only in the past few years that real-time deontic logics have been developed to reason about time quantitatively. In this paper we present timed contract automata, an automata-based deontic modelling approach complementing these logics with a more operational view of such normative clauses and providing a computational model more amenable to automated analysis and monitoring.},
pdf = {}
}
@article{HMR+22csm,
author = {William Hughes and Tobias Magnusson and Alejandro Russo and Gerardo Schneider},
title = {Cheap and secure metatransactions on the blockchain using hash-based authorisation and preferred batchers},
journal = {Blockchain: Research and Applications},
publisher = {Elsevier},
year = {2022},
issn = {2096-7209},
optkey = {},
optvolume = {},
optnumber = {},
optpages = {},
month = {December},
note = {In Press, available online},
doi = {10.1016/j.bcra.2022.100125},
keywords = {Ethereum, Domain-specific language, Interpreter, Gas optimisation},
abstract = {Smart contracts are self-executing programs running in the blockchain allowing for decentralised storage and execution without a middleman. On-chain execution is expensive, with miners charging fees for distributed execution according to a cost model defined in the protocol. In particular, transactions have a high fixed cost. We present MultiCall, a transaction-batching interpreter for Ethereum that reduces the cost of smart contract executions by gathering multiple users’ transactions into a batch. Our current implementation of MultiCall includes the following features: the ability to emulate Ethereum call and create transactions, both from MultiCall itself and using an identity unique to the user; the ability to cheaply pay ether to other MultiCall users; and the ability to authorise emulated transactions on behalf of multiple users in a single transaction using hash-based authorisation rather than more expensive signatures. This improves upon on a previous version of MultiCall. Our experiments show that MultiCall provides a saving between 57\% and 99\% of the fixed transaction cost compared with the standard approach of sending Ethereum transactions directly. Besides, we also show how to prevent an economic attack exploiting the metatransaction feature, describe a generic protocol for hash-based authorisation of metatransactions, and analyse how to minimise its off-chain computational and storage cost.},
pdf = {}
}
@article{AJO+22sab,
author = {Hamed Arshad and
Christian Johansen and
Olaf Owe and
Pablo Picazo{-}Sanchez and
Gerardo Schneider},
title = {Semantic Attribute-Based Encryption: {A} framework for combining {ABE} schemes with semantic technologies},
journal = {Information Sciences},
volume = {616},
pages = {558--576},
year = {2022},
url = {https://doi.org/10.1016/j.ins.2022.10.132},
doi = {10.1016/j.ins.2022.10.132},
abstract = {Attribute-Based Encryption (ABE) is a cryptographic solution to protect resources in a fine-grained manner based on a set of public attributes. This is similar to attribute-based access control schemes in the sense that both rely on public attributes and access control policies to grant access to resources. However, ABE schemes do not consider the semantics of attributes provided by users or required by access structures. Such semantics not only improve the functionality by making proper access decisions but also enable cross-domain interoperability by making users from one domain able to access and use resources of other domains. This paper proposes a Semantic ABE (SABE) framework by augmenting a classical Ciphertext-Policy ABE (CP-ABE) scheme with semantic technologies using a generic procedure by which any CP-ABE scheme can be extended to an SABE. The proposed SABE framework is implemented in Java and the source code is publicly available. The experiment results confirm that the performance of the proposed framework is promising.},
pdf = {}
}
@book{RCS+22fm,
author = {Markus Roggenbach and
Antonio Cerone and
Bernd{-}Holger Schlingloff and
Gerardo Schneider and
Siraj Ahmed Shaikh},
title = {Formal Methods for Software Engineering - Languages, Methods, Application Domains},
series = {Texts in Theoretical Computer Science. An {EATCS} Series},
publisher = {Springer},
year = {2022},
opturl = {https://doi.org/10.1007/978-3-030-38800-3},
doi = {10.1007/978-3-030-38800-3},
isbn = {978-3-030-38799-0},
abstract = {Software programs are formal entities with precise meanings independent of their programmers, so the transition from ideas to programs necessarily involves a formalisation at some point.
The first part of this graduate-level introduction to formal methods develops an understanding of what constitutes formal methods and what their place is in Software Engineering. It also introduces logics as languages to describe reasoning and the process algebra CSP as a language to represent behaviours. The second part offers specification and testing methods for formal development of software, based on the modelling languages CASL and UML. The third part takes the reader into the application domains of normative documents, human machine interfaces, and security. Use of notations and formalisms is uniform throughout the book.},
pdf = {}
}
@article{JPF+22mdpl,
author = {Johanna Johansen and
Tore Pedersen and
Simone Fischer{-}H{\"{u}}bner and
Christian Johansen and
Gerardo Schneider and
Arnold Roosendaal and
Harald Zwingelberg and
Anders Jakob Sivesind and
Josef Noll},
title = {A multidisciplinary definition of privacy labels},
journal = {Inf. Comput. Secur.},
volume = {30},
number = {3},
pages = {452--469},
year = {2022},
opturl = {https://doi.org/10.1108/ICS-06-2021-0080},
doi = {10.1108/ICS-06-2021-0080},
pdf = {ICS2022.pdf},
abstract = {Privacy is currently in distress and in need of rescue, much like princesses in the allfamiliar fairytales. We employ storytelling and metaphors from fairytales to make reader-friendly and streamline our arguments about how a complex concept of Privacy Labeling (the ‘knight in shining armor’) can be a solution to the current state of Privacy (the ‘princess in distress’). We give a precise definition of Privacy Labeling (PL), painting a panoptic portrait from seven different perspectives (the ‘seven helpers’): Business, Legal, Regulatory, Usability and Human Factors, Educative, Technological, and Multidisciplinary. We describe a common vision, proposing several important ‘traits of character’ of PL as well as identifying ‘undeveloped potentialities’, i.e., open problems on which the community can focus. More specifically, this position paper identifies the stakeholders of the PL and their needs with regard to privacy, describing how PL should be and look like in order to address these needs. Throughout the paper, we highlight goals, characteristics, open problems, and starting points for creating, what we consider to be, the ideal PL. In the end we present three approaches to establish and manage PL, through: self-evaluations, certifications, or community endeavors. Based on these, we sketch a roadmap for future developments.}
}
@inproceedings{ASS21rpa,
author = {Hanaa Alshareef and
Sandro Stucki and
Gerardo Schneider},
opteditor = {Radu Calinescu and
Corina S. Pasareanu},
title = {Refining Privacy-Aware Data Flow Diagrams},
booktitle = {19th International Conference Software Engineering and Formal Methods ({SEFM}'21), Virtual Event, December 6-10, 2021},
optbooktitle = {{SEFM}'21},
series = {LNCS},
volume = {13085},
pages = {121--140},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-92124-8\_8},
doi = {10.1007/978-3-030-92124-8\_8},
optannote = {Virtual Event, December 6-10, 2021}
}
@article{SSS+21gbm,
author = {Stucki, Sandro and S{\'a}nchez, C{\'e}sar and Schneider, Gerardo and Bonakdarpour, Borzoo},
doi = {10.1007/s10703-020-00358-w},
isbn = {1572-8102},
journal = {Formal Methods in System Design},
title = {Gray-box monitoring of hyperproperties with an application to privacy},
volume = {58},
number = {1-2},
pages = {126--159},
url = {https://doi.org/10.1007/s10703-020-00358-w},
year = {2021},
abstract = {Runtime verification is a complementary approach to testing, model checking and other static verification techniques to verify software properties. Monitorability characterizes what can be verified (monitored) at run time. Different definitions of monitorability have been given both for trace properties and for hyperproperties (properties defined over sets of traces), but these definitions usually cover only some aspects of what is important when characterizing the notion of monitorability. The first contribution of this paper is a refinement of classic notions of monitorability both for trace properties and hyperproperties, taking into account, among other things, the computability of the monitor. A second contribution of our work is to show that black-box monitoring of HyperLTL (a logic for hyperproperties) is in general unfeasible, and to suggest a gray-box approach in which we combine static and runtime verification. The main idea is to call a static verifier as an oracle at run time allowing, in some cases, to give a final verdict for properties that are considered to be non-monitorable under a black-box approach. Our third contribution is the instantiation of this solution to a privacy property called distributed data minimization which cannot be verified using black-box runtime verification. We use an SMT-based static verifier as an oracle at run time. We have implemented our gray-box approach for monitoring data minimization into the proof-of-concept tool Minion. We describe the tool and apply it to a few case studies to show its feasibility.},
pdf = {}
}
@inproceedings{KLS21tddl,
author = {Karam Younes Kharraz and Martin Leucker and Gerardo Schneider},
title = {Timed Dyadic Deontic Logic},
booktitle = {The 34th International Conference on Legal Knowledge and Information Systems (JURIX'21)},
year = {2021},
opteditor = {},
volume = {346},
series = {Frontiers in Artificial Intelligence and Applications},
pages = {197--204},
abstract = {In this paper, we introduce TDDL, a timed dyadic deontic logic. Our starting point is a version of a dyadic deontic logic with conditional obligations, permissions, and obligations, and with a ``reparation'' operator for representing contrary-to-duties and contrary-to-prohibitions. We also consider a sequence operator allowing us to define norms as sequences of individual norms and most importantly with timed intervals, allowing us to express deadlines of norms. We provide a trace semantics capturing both satisfaction and violation of norms and discuss fulfillment of TDDL specifications.},
publisher = {IOS Press},
doi = {10.3233/FAIA210336},
pdf = {jurix2021.pdf}
}
@inproceedings{CPS21pob,
author = {Christian Colombo and
Gordon J. Pace and
Gerardo Schneider},
opteditor = {Ezio Bartocci and
Yli{\`{e}}s Falcone and
Martin Leucker},
title = {Runtime Verification: Passing on the Baton},
booktitle = {Formal Methods in Outer Space - Essays Dedicated to Klaus Havelund on the Occasion of His 65th Birthday},
series = {LNCS},
volume = {13065},
pages = {89--107},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-87348-6\_5},
doi = {10.1007/978-3-030-87348-6\_5},
abstract = {Twenty years have passed since the first workshop on runtime verification—the area has grown and evolved with hundreds of papers published and a sizeable number of mature tools developed. In a special occasion like this it is good to look back, but it is also good to look forward to the future. In this paper, we outline a very brief history of runtime verification, and propose a way of passing the knowledge down to future generations of academics and industry practitioners in the form of a roadmap for teaching runtime verification. The proposal, based on our experience, not only equips students with the fundamental theory underpinning runtime verification, but also ensures they have the required skills to engineer it into industrial systems. Our hope is that this would increase uptake and eventually give rise to the establishment of industry-grade tools.}
}
@inproceedings{APSS21smt,
author = {Shaun Azzopardi and
Gordon J. Pace and
Fernando Schapachnik and
Gerardo Schneider},
opteditor = {Lu Feng and
Dana Fisman},
title = {On the Specification and Monitoring of Timed Normative Systems},
booktitle = {21st International Conference on Runtime Verification ({RV}'21), Virtual Event},
optbooktitle = {21st International Conference on Runtime Verification ({RV}'21), Virtual Event, October 11-14, 2021},
series = {LNCS},
volume = {12974},
pages = {81--99},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-88494-9\_5},
doi = {10.1007/978-3-030-88494-9\_5},
abstract = {In this article we explore different issues and design choices that arise when considering how to fully embrace timed aspects in the formalisation of normative systems, e.g., by using deontic modalities, looking primarily through the lens of monitoring. We primarily focus on expressivity and computational aspects, discussing issues such as duration, superposition, conflicts, attempts, discharge, and complexity, while identifying semantic choices which arise and the challenges these pose for full monitoring of legal contracts.},
pdf = {rv21.pdf}
}
@inproceedings{ZGS+21amu,
author = {Sebasti{\'{a}}n Zudaire and
Felipe Gorostiaga and
C{\'{e}}sar S{\'{a}}nchez and
Gerardo Schneider and
Sebasti{\'{a}}n Uchitel},
title = {Assumption Monitoring Using Runtime Verification for {UAV} Temporal Task Plan Executions},
booktitle = {{IEEE} International Conference on Robotics and Automation, {ICRA} 2021, Xi'an, China, May 30 - June 5, 2021},
pages = {6824--6830},
publisher = {{IEEE}},
year = {2021},
url = {https://doi.org/10.1109/ICRA48506.2021.9561671},
doi = {10.1109/ICRA48506.2021.9561671},
abstract = {Temporal task planning guarantees a robot will succeed in its task as long as certain explicit and implicit assumptions about the robot's operating environment, sensors, and capabilities hold. A robot executing a plan can silently fail to fulfill the task if the assumptions are violated at runtime. Monitoring assumption violations at runtime can flag silent failures and also provide mitigation and remediation opportunities. However, this requires means for describing assumptions combining temporal and quantitative data, automatic construction of correct monitors and ensuring a correct interplay between the planning execution and monitors. In this paper we propose combining temporal planning with stream runtime verification, which offers a high-level language to describe monitors together with guarantees on execution time and memory usage. We demonstrate our approach both in real and simulated flights for some typical mission scenarios.},
pdf = {icra21.pdf}
}
@inproceedings{APS21imr,
author = {Shaun Azzopardi and
Nir Piterman and
Gerardo Schneider},
opteditor = {Zhe Hou and
Vijay Ganesh},
title = {Incorporating Monitors in Reactive Synthesis Without Paying the Price},
booktitle = {19th International Symposium on Automated Technology for Verification and Analysis ({ATVA}'21), Gold Coast, QLD, Australia, October 18-22, 2021},
series = {LNCS},
volume = {12971},
pages = {337--353},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-88885-5\_22},
doi = {10.1007/978-3-030-88885-5\_22},
abstract = {Temporal synthesis attempts to construct reactive programs that satisfy a given declarative (LTL) formula. Practitioners have found it challenging to work exclusively with declarative specifications, and have found languages that combine modelling with declarative specifications more useful. Synthesised controllers may also need to work with pre-existing or manually constructed programs.In this paper we explore an approach that combines synthesis of declarative specifications in the presence of an existing behaviour model as a monitor, with the benefit of not having to reason about the state space of the monitor. We suggest a formal language with automata monitors as non-repeating and repeating triggers for LTL formulas. We use symbolic automata with memory as triggers, resulting in a strictly more expressive and succinct language than existing regular expression triggers. We give a compositional synthesis procedure for this language, where reasoning about the monitor state space is minimal. To show the advantages of our approach we apply it to specifications requiring counting and constraints over arbitrarily long sequence of events, where we can also see the power of parametrisation, easily handled in our approach. We provide a tool to construct controllers (in the form of symbolic automata) for our language.},
pdf = {atva21.pdf}
}
@inproceedings{HRS21multi,
author = {William Hughes and
Alejandro Russo and
Gerardo Schneider},
opteditor = {Keke Gai and
Kim{-}Kwang Raymond Choo},
title = {MultiCall: {A} Transaction-batching Interpreter for Ethereum},
booktitle = {{BSCI}'21: Proceedings of the 3rd {ACM} International Symposium on Blockchain and Secure Critical Infrastructure, Virtual Event, Hong Kong, June 7, 2021},
pages = {25--35},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3457337.3457839},
doi = {10.1145/3457337.3457839},
pdf = {bsci21.pdf},
optaddress = {Virtual Event, Hong Kong},
abstract = {Smart contracts are self-executing programs running in the blockchain allowing for decentralised storage and execution without a middleman. On-chain execution is expensive, with miners charging fees for distributed execution according to a cost model defined in the protocol. In particular, transactions have a high fixed cost. In this paper we present MultiCall, an interpreter that reduces the cost of smart contract execution by emulating sequences of transactions from multiple users in one transaction. We have implemented and integrated MultiCall into Ethereum. Our evaluation shows that using MultiCall provides a saving between 56.8\% and 98.9\% of the fixed per-Transaction cost compared to the standard approach of sending transactions individually.}
}
@inproceedings{ASS21tdf,
author = {Hanaa Alshareef and
Sandro Stucki and
Gerardo Schneider},
opteditor = {Slimane Hammoudi and
Lu{\'{\i}}s Ferreira Pires and
Edwin Seidewitz and
Richard Soley},
title = {Transforming Data Flow Diagrams for Privacy Compliance},
booktitle = {9th International Conference on Model-Driven Engineering and Software Development ({MODELSWARD'21})},
pages = {207--215},
publisher = {{SCITEPRESS}},
year = {2021},
isbn = {978-989-758-487-9},
issn = {2184-4348},
url = {https://doi.org/10.5220/0010255002070215},
doi = {10.5220/0010255002070215},
abstract = {Most software design tools, as for instance Data Flow Diagrams (DFDs), are focused on functional aspects and cannot thus model non-functional aspects like privacy. In this paper, we provide an explicit algorithm and a proof-of-concept implementation to transform DFDs into so-called Privacy-Aware Data Flow Diagrams (PA-DFDs). Our tool systematically inserts privacy checks to a DFD, generating a PA-DFD. We apply our approach to two realistic applications from the construction and online retail sectors.},
pdf = {modelsward2021.pdf},
optnote = { Online Streaming, February 8-10, 2021}
}
@inproceedings{PSS20hsp,
author = {Pablo Picazo{-}Sanchez and
Gerardo Schneider and
Andrei Sabelfeld},
opteditor = {Stephan Krenn and
Haya Shulman and
Serge Vaudenay},
title = {{HMAC} and "Secure Preferences": Revisiting Chromium-Based Browsers Security},
booktitle = {19th International Conference on Cryptology and Network Security ({CANS'20})},
series = {LNCS},
volume = {12579},
pages = {107--126},
publisher = {Springer},
year = {2020},
url = {https://doi.org/10.1007/978-3-030-65411-5\_6},
doi = {10.1007/978-3-030-65411-5\_6},
abstract = {Google disabled years ago the possibility to freely modify some internal configuration parameters, so options like silently (un)install browser extensions, changing the home page or the search engine were banned. This capability was as simple as adding/removing some lines from a plain text file called Security Preference File (SPF) automatically created by Chromium the first time it was launched. Concretely, Google introduced a security mechanism based on a cryptographic algorithm named HMAC to avoid users and applications other than the browser modifying the SPF. This paper demonstrates that it is possible to perform browser hijacking, browser extension fingerprinting, and remote code execution attacks as well as silent browser extensions (un)installation by coding a platform-independent proof-of-concept changeware that exploits the HMAC, allowing for free modification of the SPF. Last but not least, we analyze the security of the four most important Chromium-based browsers: Brave, Chrome, Microsoft Edge, and Opera, concluding that all of them suffer from the same security pitfall.},
pdf = {CANS2020.pdf}
}
@inproceedings{KOS20ifc,
author = {Farzane Karami and
Olaf Owe and
Gerardo Schneider},
opteditor = {Mikael Asplund and
Simin Nadjm{-}Tehrani},
title = {Information-Flow Control by Means of Security Wrappers for Active
Object Languages with Futures},
booktitle = {25th Nordic Conference on Secure {IT} Systems (NordSec'20)},
series = {LNCS},
volume = {12556},
pages = {74--91},
publisher = {Springer},
year = {2020},
url = {https://doi.org/10.1007/978-3-030-70852-8\_5},
doi = {10.1007/978-3-030-70852-8\_5},
abstract = {This paper introduces a run-time mechanism for preventing leakage of secure information in distributed systems. We consider a general concurrency language model where concurrent objects interact by asynchronous method calls and futures. The aim is to prevent leakage of secure information to low-level viewers. The approach is based on a notion of security wrappers, where a wrapper encloses an object or a component and controls its interactions with the environment. Our run-time system automatically adds a wrapper to an insecure component.The wrappers are invisible such that a wrapped component and its environment are not aware of it.
The security policies of a wrapper are formalized based on a notion of security levels. At run-time, future components will be wrapped upon need, and objects of unsafe classes will be wrapped, using static checking to limit the number of unsafe classes and thereby reducing run-time overhead. We define an operational semantics and sketch a proof of non-interference. A service provider may use wrappers to protect its services in an insecure environment, and vice-versa: a system platform may use wrappers to protect itself from insecure service providers.},
pdf = {nordsec2020.pdf}
}
@inproceedings{PSS20rsc,
author = {Gordon J. Pace and
C{\'{e}}sar S{\'{a}}nchez and
Gerardo Schneider},
opteditor = {Tiziana Margaria and
Bernhard Steffen},
title = {Reliable Smart Contracts},
booktitle = {Leveraging Applications of Formal Methods, Verification and Validation:
Applications - 9th International Symposium on Leveraging Applications
of Formal Methods, ISoLA 2020, Proceedings, Part {III}},
series = {LNCS},
volume = {12478},
pages = {3--8},
publisher = {Springer},
optmonth = {October 20-30},
year = {2020},
optaddress = {Rhodes, Greece},
issn = {03029743},
url = {https://doi.org/10.1007/978-3-030-61467-6\_1},
doi = {10.1007/978-3-030-61467-6\_1},
abstract = {The rise of smart contracts executed on blockchain and other distributed ledger technologies enabled trustless yet decentralised computation. Various applications take advantage of this computational model, including enforced financial contracts, self-sovereign identity and voting. But smart contracts are nothing but software running on a blockchain, with risks of malfunction due to bugs in the code. Compared to traditional systems, there is an additional risk in that erroneous computation or transactions triggered by a smart contract cannot be easily rolled back due to the immutability of the underlying execution model. This ISoLA track brings together a number of experts in the field of smart contract reliability and verification to discuss the state-of-the-art in smart contract dependability and discuss research challenges and future directions.
},
pdf = {isola2020-RSC-Intro.pdf}
}
@inproceedings{MNPS20,
author = {Piergiuseppe Mallozzi and Pierluigi Nuzzo and Patrizio Pelliccione and Gerardo Schneider},
title = {CROME: Contract-Based Robotic Mission Specification},
booktitle = {18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE'20)},
year = {2020},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
pages = {1--11},
url = {https://doi.org/10.1109/MEMOCODE51338.2020.9315065},
doi = {10.1109/MEMOCODE51338.2020.9315065},
optmonth = {},
optaddress = {Jaipur, India},
optorganization = {},
publisher = {IEEE},
isbn = {},
abstract = {We address the problem of automatically constructing a formal robotic mission specification in a logic language with precise semantics starting from an informal description of the mission requirements. We present CROME (Contract-based RObotic Mission spEcification), a framework that allows capturing mission requirements in terms of goals by using specification patterns, and automatically building linear temporal logic mission specifications conforming with the requirements. CROME leverages a new formal model, termed Contract-based Goal Graph (CGG), which enables organizing the requirements in a modular way with a rigorous compositional semantics. By relying on the CGG, it is then possible to automatically: i) check the \textit{feasibility} of the overall mission, ii) further \textit{refine} it from a library of pre-defined goals, and iii) \textit{synthesize} multiple controllers that implement different parts of the mission at different abstraction levels, when the specification is realizable. If the overall mission is not realizable, CROME identifies mission scenarios, i.e., sub-missions that can be realizable. We illustrate the effectiveness of our methodology and supporting tool on a case study.},
pdf = {memocode2020.pdf}
}
@article{APP+20cac,
author = {Hanaa Alshareef and Ra{\'{u}}l Pardo and Pablo Picazo-Sanchez and Gerardo Schneider},
title = {A Collaborative Access Control Framework for Online Social Networks},
journal = {Journal of Logical and Algebraic Methods in Programming},
volume = {114},
pages = {},
month = {May},
year = {2020},
url = {https://doi.org/10.1016/j.jlamp.2020.100562},
doi = {10.1016/j.jlamp.2020.100562},
issn = {2352-2208},
abstract = {Most Online Social Networks allow users to set their privacy settings concerning posting information, but current implementations do not allow a fine grained enforcement in case the posted item concerns other users. In this paper we propose a new collaborative access control framework that takes into account the relation of multiple users for viewing as well as for sharing items, eventually solving conflicts in the privacy settings of the users involved. Our solution relies on two algorithms, one for viewing and another one for sharing items. We provide an evaluation of these algorithms where we demonstrate how varying some of the parameters directly influences the decision of viewing or sharing an item. Last but not least, we present a proof-of-concept implementation of our approach in an open source social network called Diaspora.},
pdf = {jlamp2020.pdf}
}
@article{PTS20ayp,
author = {Pablo Picazo{-}Sanchez and
Juan Tapiador and
Gerardo Schneider},
title = {After You, Please: Browser Extensions Order Attacks and Countermeasures},
journal = {International Journal of Information Security},
optjournal = {Int. J. Inf. Sec.},
volume = {19},
number = {6},
pages = {623--638},
year = {2020},
url = {https://doi.org/10.1007/s10207-019-00481-8},
doi = {10.1007/s10207-019-00481-8},
abstract = {Browser extensions are small applications executed in the browser context that provide additional capabilities and enrich the user experience while surfing the web. The acceptance of extensions in current browsers is unquestionable. For instance, Chrome's official extension repository has more than 63,000 extensions, with some of them having more than 10M users. When installed, extensions are pushed into an internal queue within the browser. The order in which each extension executes depends on a number of factors, including their relative installation times. In this paper, we demonstrate how this order can be exploited by an unprivileged malicious extension (i.e., one with no more permissions than those already assigned when accessing web content) to get access to any private information that other extensions have previously introduced. We propose a solution that does not require modifying the core browser engine, since it is implemented as another browser extension. We prove that our approach effectively protects the user against usual attackers (i.e., any other installed extension) as well as against strong attackers having access to the effects of all installed extensions (i.e., knowing who did what). We also prove soundness and robustness of our approach under reasonable assumptions.},
issn = {1615-5270},
pdf = {InfSec2020.pdf}
}
@article{OPP+19fai,
author = {Lara Ortiz{-}Martin and
Pablo Picazo{-}Sanchez and
Pedro Peris{-}Lopez and
Juan Tapiador and
Gerardo Schneider},
title = {Feasibility Analysis of Inter-Pulse Intervals Based Solutions for
Cryptographic Token Generation by Two Electrocardiogram Sensors},
journal = {Future Generation Comp. Syst.},
volume = {96},
pages = {283--296},
year = {2019},
url = {https://doi.org/10.1016/j.future.2019.02.021},
doi = {10.1016/j.future.2019.02.021},
abstract = {In this paper we address the problem of how two devices that are sensing the same heart signal can generate the same cryptographic token by extracting them from the Inter-Pulse Intervals (IPIs) of each cardiac signal. Our analysis is based on the use of a run-time monitor, which is extracted from a formal model and verified against predefined properties, combined with a fuzzy extractor to improve the final result. We first show that it is impossible, in general, to correct the differences between the IPIs derived from two captured electrocardiogram (ECG) signals when using only error correction techniques, thus being impossible to corroborate previous claims on the feasibility of this approach. Then, we provide a large-scale evaluation of the proposed method (run-time monitor and fuzzy extractor) over 19 public databases from the Physionet repository containing heart signals. The results clearly show the practicality of our proposal achieving a 91\% of synchronization probability for healthy individuals. Additionally, we also conduct an experiment to check how long the sensors should record the heart signal in order to generate tokens of 32, 64 and 128 bits. Contrarily to what it is usually assumed (6, 12, and 24 s for individuals with a heart rate of 80 beats-per-minute), the sensors have to wait 13, 28 and 56.5 s on median, respectively, to derive the same token from both sensors.},
pdf = {fgcs2019.pdf}
}
@inproceedings{ABE+19vsc,
author = {Wolfgang Ahrendt and Richard Bubel and Joshua Ellul and Gordon J. Pace and Ra{\'{u}}l Pardo and Vincent Rebiscoul and Gerardo Schneider},
title = {Verification of Smart Contract Business Logic: Exploiting a Java Source Code Verifier},
booktitle = {Eigth International Conference on Fundamentals of Software Engineering (FSEN'19)},
year = {2019},
opteditor = {},
volume = {11761},
optnumber = {},
series = {LNCS},
pages = {228--243},
optmonth = {},
optaddress = {Tehran, Iran},
optorganization = {},
publisher = {Springer},
doi = {10.1007/978-3-030-31517-7\_16},
isbn = {978-3-030-31516-0},
abstract = {Smart contracts have been argued to be a means of building trust between parties by providing a self-executing equivalent of legal contracts. And yet, code does not always perform what it was originally intended to do, which resulted in losses of millions of dollars. Static verification of smart contracts is thus a pressing need. This paper presents an approach to verifying smart contracts written in Solidity by automatically translating Solidity into Java and using KeY, a deductive Java verification tool. In particular, we solve the problem of rolling back the effects of aborted transactions by exploiting KeY's native support of JavaCard transactions. We apply our approach to a smart contract which automates a casino system, and discuss how the approach addresses a number of known shortcomings of smart contract development in Solidity.},
pdf = {fsen19.pdf}
}
@inproceedings{MCP+19rmf,
author = {Piergiuseppe Mallozzi and
Ezequiel Castellano and
Patrizio Pelliccione and
Gerardo Schneider and
Kenji Tei},
title = {A runtime monitoring framework to enforce invariants on reinforcement learning agents exploring complex environments},
booktitle = {Proceedings of the 2nd International Workshop on Robotics Software
Engineering (RoSE@ICSE 2019)},
optaddress = {Montreal,Canada},
pages = {5--12},
year = {2019},
url = {https://dl.acm.org/citation.cfm?id=3340891},
doi = {10.1109/RoSE.2019.00011},
publisher = {{IEEE} / {ACM}},
abstract = {Without prior knowledge of the environment, a software agent can learn to achieve a goal using machine learning. Model-free Reinforcement Learning (RL) can be used to make the agent explore the environment and learn to achieve its goal by trial and error.
Discovering effective policies to achieve the goal in a complex environment is a major challenge for RL.
Furthermore, in safety-critical applications, such as robotics, an unsafe action may cause catastrophic consequences in the agent or in the environment.
In this paper, we present an approach that uses runtime monitoring to prevent the reinforcement learning agent to perform ``wrong" actions and to exploit prior knowledge to smartly explore the environment.
Each monitor is defined by a property that we want to enforce to the agent and a context.
The monitors are orchestrated by a meta-monitor that activates and deactivates them dynamically according to the context in which the agent is learning.
We have evaluated our approach by training the agent in randomly generated learning environments. Our results show that our approach blocks the agent from performing dangerous and safety-critical actions in all the generated environments.
Besides, our approach helps the agent to achieve its goal faster by providing feedback and shaping its reward during learning.},
pdf = {RoSE19.pdf}
}
@inproceedings{SSS+gbm,
author = {Sandro Stucki and C\'esar S\'anchez and Gerardo Schneider and Borzoo Bonakdarpour},
title = {Gray-box Monitoring of Hyperproperties},
booktitle = {Formal Methods (FM'19)},
year = {2019},
opteditor = {Maurice H. ter Beek and Annabelle McIver and Jos{\'{e}} N. Oliveira},
volume = {11800},
series = {LNCS},
pages = {406--424},
optmonth = {},
publisher = {Springer},
eisbn = {978-3-030-30942-8},
isbn = {978-3-030-30941-1},
issn = {0302-9743},
doi = {10.1007/978-3-030-30942-8\_25},
abstract = {Many important system properties, particularly in security and
privacy, cannot be verified statically.
Therefore, runtime verification is an appealing alternative.
Logics for hyperproperties, such as HyperLTL, support a
rich set of such properties.
We first show that black-box monitoring of HyperLTL is in general
unfeasible, and suggest a gray-box approach.
Gray-box monitoring implies performing analysis of the system at
run-time, which brings new limitations to monitorabiliy (the
feasibility of solving the monitoring problem).
Thus, as another contribution of this paper, we refine the classic
notions of monitorability, both for trace properties and
hyperproperties, taking into account the computability of the
monitor.
We then apply our approach to monitor a privacy hyperproperty called
distributed data minimality, expressed as a HyperLTL property,
by using an SMT-based static verifier at runtime.
},
pdf = {fm2019.pdf}
}
@techreport{PST19ayp,
author = {Pablo Picazo-S\'anchez and Gerardo Schneider and Juan Tapiador},
title = {After You, Please: Browser Extensions Order Attacks and Countermeasures},
institution = {CoRR - arXiv.org},
year = {2019},
archiveprefix = {arXiv},
url = { http://arxiv.org/abs/1908.02205},
number = {abs/1908.02205},
month = {August}
}
@article{SSA+19ASC,
author = {C\'esar S\'anchez and
Gerardo Schneider and
Wolfgang Ahrendt and
Ezio Bartocci and
Domenico Bianculli and
Christian Colombo and
Yli\'es Falcone and
Adrian Francalanza and
Srdan Krsti\'{c} and
Dejan Nickovic and
Gordon J.~Pace and
Jose Rufino and
Julien Signoles and
Dmitriy Traytel and
Alexander Weiss},
title = {{A Survey of Challenges for Runtime Verification from
Advanced Application Domains (Beyond Software)}},
journal = {Formal Methods in System Design},
year = {2019},
month = {August},
volume = {54},
number = {3},
pages = {279--335},
publisher = {Springer},
doi = {10.1007/s10703-019-00337-w},
optisbn = {},
e-issn = {1572-8102},
issn = {0925-9856},
note = {Open source, freely available at \url{https://rdcu.be/bOhjI}},
abstract = {Runtime verification is an area of formal methods that studies the
dynamic analysis of execution traces against formal specifications.
Typically, the two main activities in runtime verification efforts
are the process of creating monitors from specifications, and the
algorithms for the evaluation of traces against the generated
monitors.
Other activities involve the instrumentation of the system to
generate the trace and the communication between the system under
analysis and the monitor.
Most of the applications in runtime verification have been focused
on the dynamic analysis of software, even though there are many more
potential applications to other computational devices and target
systems.
In this paper we present a collection of challenges for runtime
verification extracted from concrete application domains, focusing
on the difficulties that must be overcome to tackle these specific
challenges.
The computational models that characterize these domains require to
devise new techniques beyond the current state of the art in runtime
verification.},
pdf = {fmsd2019.pdf}
}
@inproceedings{CFL+18cost,
author = {Christian Colombo and
Yli{\`{e}}s Falcone and
Martin Leucker and
Giles Reger and
C{\'{e}}sar S{\'{a}}nchez and
Gerardo Schneider and
Volker Stolz},
title = {{COST} Action {IC1402} Runtime Verification Beyond Monitoring},
booktitle = {18th International Conference on Runtime Verification (RV'18)},
pages = {18--26},
year = {2018},
doi = {10.1007/978-3-030-03769-7\_2},
series = {LNCS},
volume = {11237},
publisher = {Springer},
pdf = {RV18-ARVI_report.pdf},
abstract = {In this paper we report on COST Action IC1402 which studies Runtime Verification approaches beyond Monitoring. COST Actions are funded by the European Union and are an efficient networking instrument for researchers, engineers and scholars to cooperate and coordinate research activities. This COST action IC1402 lasted over the past four years, involved researchers from 27 different European countries and Australia and allowed to have many different working group meetings, workshops and individual visits.}
}
@inproceedings{PRS+18sp,
author = {Srinivas Pinisetty and
Partha S. Roop and
Vidula Sawant and
Gerardo Schneider},
title = {Security of Pacemakers using Runtime Verification},
booktitle = {16th ACM/IEEE International Conference on Formal Methods and Models
for System Design (MEMOCODE'18)},
pages = {51--61},
year = {2018},
doi = {10.1109/MEMCOD.2018.8556922},
publisher = {{IEEE}},
abstract = {The US Food and Drug Administration (FDA) recently recalled
approximately 465,000 pacemakers that were vulnerable to hacking. It
was reported that hackers could either pace the devices rapidly
inducing arrhythmia or could drain the battery. Such actions
would compromise the health and well being of the patient concerned.
Considering this, techniques to ensure the security of implantable
medical devices is an emerging area of research. To the best of our
knowledge, existing techniques lack the formal rigour for ensuring the
safety and security of such systems. While methods exist for formal
verification of pacemaker software, these are not suitable to prevent
security vulnerabilities. To this end we develop a run-time
verification based approach. Our approach proposes a wearable device
that non-invasively senses the familiar ECG signals in order to
determine if a pacemaker has been compromised. We develop a set of
timed policies to be monitored at run-time. We provide a
methodology for the design of the wearable device and results demonstrate the
technical feasibility of the developed concept.},
isbn = {},
pdf = {memocode18.pdf}
}
@inproceedings{APS18sc,
author = {Wolfgang Ahrendt and
Gordon J. Pace and
Gerardo Schneider},
title = {Smart Contracts: {A} Killer Application for Deductive Source Code
Verification},
booktitle = {Principled Software Development - Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of his 60th Birthday},
pages = {1--18},
year = {2018},
doi = {10.1007/978-3-319-98047-8\_1},
opteditor = {Peter M{\"{u}}ller and Ina Schaefer},
publisher = {Springer},
abstract = {Smart contracts are agreements between parties which, not only describe the ideal behaviour expected from those parties, but also automates such ideal performance. Blockchain, and similar distributed ledger technologies have enabled the realisation of smart contracts without the need of trusted parties --- typically using computer programs which have access to digital assets to describe smart contracts, storing and executing them in a transparent and immutable manner on a blockchain.
Many approaches have adopted fully fledged programming languages to describe smart contract, thus inheriting from software the challenge of correctness and verification --- just as in software systems, in smart contracts mistakes happen easily, leading to unintended and undesirable behaviour. Such wrong behaviour may show accidentally, but as the contract code is public, malicious users can seek for vulnerabilities to exploit, causing severe damage. This is witnessed by the increasing number of
real world incidents, many leading to huge financial losses.
As in critical software, the formal verification of smart contracts is thus paramount.
In this paper we argue for the use of deductive software verification as a way to increase confidence in the correctness of smart contracts. We describe challenges and opportunities, and a concrete research program, for deductive source code level verification, focussing on the most widely used smart contract platform and language, Ethereum and Solidity.},
isbn = {978-3-319-98046-1},
pdf = {Arnd_60Festschrift2018.pdf}
}
@inproceedings{schneider18pbd,
author = {Gerardo Schneider},
title = {{Is Privacy by Construction Possible?}},
booktitle = {8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation - Track: X-by-Construction (ISoLA'18, part I},
series = {LNCS},
volume = {11244},
pages = {471-485},
year = {2018},
doi = {10.1007/978-3-030-03418-4\_28},
publisher = {Springer},
issn = {0302-9743},
isbn = {978-3-030-03417-7},
abstract = {Finding suitable ways to handle personal data in conformance with the law is challenging.
The European General Data Protection Regulation (GDPR), enforced since May 2018, makes it mandatory to citizens and companies to comply with the privacy requirements set in the regulation.
For existing systems the challenge is to be able to show evidence that they are already complying with the GDPR, or otherwise to work towards compliance by modifying their systems and procedures, or alternatively reprogramming their systems in order to pass the eventual controls.
For those starting new projects the advice is to take privacy into consideration since the very beginning, already at design time. This has been known as Privacy by Design (PbD). The main question is how much privacy can you effectively achieve by using PbD, and
in particular whether it is possible to achieve Privacy by Construction.
In this paper I give my personal opinion on issues related to the ambition of achieving Privacy by Construction.},
pdf = {isola2018-PbD.pdf}
}
@inproceedings{PPS18mma,
author = {Gordon Pace and Pablo Picazo-Sanchez and Gerardo Schneider},
title = {{Migrating Monitors + ABE: A Suitable Combination for Secure IoT?}},
booktitle = {8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation - Track: RV-TheToP: Runtime Verification from the Theory To the industry Practice (ISoLA'18, part IV},
series = {LNCS},
volume = {11247},
pages = {19-24},
year = {2018},
doi = {10.1007/978-3-030-03427-6\_3},
publisher = {Springer},
issn = {0302-9743},
isbn = {978-3-030-03426-9},
abstract = {The rise of the Internet of Things brings about various challenges concerning safety, reliability and dependability as well as security and privacy.
Reliability and safety issues could be addressed by using different verification techniques, both statically and at runtime.
In particular, migrating monitors could effectively be used not only for verification purposes, but also as a way to gather information and to enforce certain policies.
The addition of monitors, however, might introduce additional security and privacy threats.
In this extended abstract we briefly sketch ideas on how to combine migrating monitors with a public cryptographic scheme named Attribute-Based Encryption as a way to ensure monitors are run by the right devices in a secure and private manner.},
pdf = {isola2018-MigratingMon.pdf}
}
@inproceedings{BSS18mhc,
author = {Borzoo Bonakdarpour and C\'esar S\'anchez and Gerardo Schneider},
title = {{Monitoring Hyperproperties by Combining Static Analysis and Runtime Verification}},
booktitle = {8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation - Track: A Broader View on Verification: From Static to Runtime and Back (ISoLA'18, part II)},
series = {LNCS},
volume = {11245},
pages = {8-27},
year = {2018},
doi = {10.1007/978-3-030-03421-4\_2},
publisher = {Springer},
issn = {0302-9743},
isbn = {978-3-030-03420-7},
abstract = {Hyperproperties are properties whose reasoning involve sets of
traces.
Examples of hyperproperties include information-flow security
properties, properties of coding/decoding systems, linearizability
and other consistency criteria, as well as privacy properties like
data minimality. We study the problem of runtime verification of
hyperproperties expressed as HyperLTL formulas that involve
quantifier alternation.
We first show that even for a simple class of temporal formulas,
virtually no $\forall\exists$ property can be monitored,
independently of the observations performed.
To manage this problem, we propose to use a combination of static
analysis with runtime verification. By using static analysis/verification,
one typically obtains a model of the system that allows
to limit the source of ``hypothetical'' traces to a sound
over-approximation of the traces of the system.
This idea allows to extend the effective monitorability of
hyperproperties to a larger class of systems and properties.
We exhibit some examples where instances of this idea have been
exploited, and discuss preliminary work towards a general method.
A second contribution of this paper is the idea of departing from
the convention that all traces come from executions of a single
system.
We show cases where traces are extracted from the observed traces of
agents, from projections of a single global trace, or from executions of
different (but related) programs.},
pdf = {isola2018-hyperproperties.pdf}
}
@inproceedings{MPD+18msa,
author = {Piergiuseppe Mallozzi and
Ra{\'{u}}l Pardo and
Vincent Duplessis and
Patrizio Pelliccione and
Gerardo Schneider},
title = {{MoVEMo: {A} Structured Approach for Engineering Reward Functions}},
booktitle = {Second {IEEE} International Conference on Robotic Computing ({IRC'18})},
pages = {250--257},
year = {2018},
optaddress = {Laguna Hills, CA, USA},
url = {https://doi.org/10.1109/IRC.2018.00053},
doi = {10.1109/IRC.2018.00053},
optmonth = {January 31-February 2},
publisher = {{IEEE} Computer Society},
isbn = {978-1-5386-4652-6},
abstract = {Reinforcement learning (RL) is a machine learning technique that has been increasingly used in robotic systems. In reinforcement learning, instead of manually pre-program what action to take at each step, we convey the goal a software agent in terms of reward functions. The agent tries different actions in order to maximize a numerical value, i.e. the reward.
A misspecified reward function can cause problems such as reward hacking, where the agent finds out ways that maximize the reward without achieving the intended goal.
As RL agents become more general and autonomous, the design of reward functions that elicit the desired behaviour in the agent becomes more important and cumbersome.
In this paper, we present a technique to formally express reward functions in a structured way; this stimulates a proper reward function design and as well enables the formal verification of it.
We start by defining the reward function using state machines.
In this way, we can statically check that the reward function satisfies certain properties, e.g., high-level requirements of the function to learn.
Later we automatically generate a runtime monitor---which runs in parallel with the learning agent---that provides the rewards according to the definition of the state machine and based on the behaviour of the agent.
We use the UPPAAL model checker to design the reward model and verify the TCTL properties that model high-level requirements of the reward function and LARVA to monitor and enforce the reward model to the RL agent at runtime.},
pdf = {irc2018.pdf}
}
@inproceedings{PSS18tek,
author = {Ra\'ul Pardo and C\'esar S\'anchez and Gerardo Schneider},
title = {{Timed Epistemic Knowledge Bases for Social Networks}},
booktitle = {Formal Methods (FM'18)},
pages = {185-202},
series = {LNCS},
volume = {10951},
optmonth = {July},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-95582-7\_11},
doi = {10.1007/978-3-319-95582-7\_11},
opteditor = {Klaus Havelund et al.},
publisher = {Springer},
isbn = {},
issn = {0302-9743},
optaddress = {Oxford, UK},
pdf = {fm2018.pdf},
abstract = {We present an epistemic logic equipped with time-stamps in atoms and epistemic operators, which enables reasoning about the moments at which events happen and knowledge is acquired or deduced. Our logic includes both an epistemic operator $K$ and a belief operator $B$, to capture the disclosure of inaccurate information. Our main motivation is to describe rich privacy policies in online social networks (OSNs). Most of today's privacy policy mechanisms in existing OSNs allow only static policies. In our logic it is possible to express rich {\em dynamic policies} in terms of the knowledge available to the different users and the precise time of actions and deductions. Our framework can be instantiated for different OSNs by specifying the effect of the actions in the evolution of the social network and in the knowledge disclosed to each user. We present an algorithm for deducing knowledge and propagating beliefs, which can also be instantiated with different variants of how the epistemic information is preserved through time. Policies are modelled as formulae in the logic, which are interpreted over timed traces. Finally, we show that the model checking problem for this logic, and in consequence policy conformance, is decidable.}
}
@inproceedings{cas18tms,
author = {Mauricio Chimento and Wolfgang Ahrendt and Gerardo Schneider},
title = {{Testing Meets Static and Runtime Verification}},
year = {2018},
booktitle = {{6th Conference on Formal Methods in Software Engineering (FormaliSE@ICSE'18)}},
pages = {30-39},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
optmonth = {June 2},
optorganization = {},
url = {http://doi.acm.org/10.1145/3193992.3194000},
doi = {10.1145/3193992.3194000},
publisher = {ACM},
isbn = {978-1-4503-5718-0},
abstract = {Test driven development (TDD) is a technique where test cases are used to guide the development of a system. This technique introduces several advantages at the time of developing a system, e.g. writing clean code, good coverage for the features of the system, and evolutionary development. In this paper we show how the capabilities of a testing focused development methodology based on TDD and model-based testing, can be enhanced by integrating static and runtime verification into its workflow. Considering that the desired system properties capture data- as well as control-oriented aspects, we integrate TDD with (static) deductive verification as an aid in the development of the data-oriented aspects, and we integrate model-based testing with runtime verification as an aid in the development of the control-oriented aspects. As a result of this integration, the proposed development methodology features the benefits of TDD and model-based testing, enhanced with, for instance, early detection of bugs which may be missed by TDD, regarding data aspects, and the validation of the overall system with respect to the model, regarding the control aspects.},
pdf = {formalise18-test_sta_RV.pdf}
}
@inproceedings{PSS18rvh,
author = {Srinivas Pinisetty and David Sands and Gerardo Schneider},
title = {{Runtime Verification of Hyperproperties for Deterministic Programs}},
year = {2018},
booktitle = {{6th Conference on Formal Methods in Software Engineering (FormaliSE@ICSE'18)}},
pages = {20-29},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
optmonth = {June 2},
optorganization = {},
url = {http://doi.acm.org/10.1145/3193992.3193995},
doi = {10.1145/3193992.3193995},
publisher = {ACM},
optdoi = {},
isbn = {978-1-4503-5718-0},
abstract = { In this paper, we consider the runtime verification problem of safety hyperproperties
for deterministic programs.
Several security and information-flow policies such as data minimality, non-interference, integrity, and software doping are naturally expressed formally as safety hyperproperties.
Although there are monitoring results for hyperproperties, the algorithms are very complex since these are properties over {\em set of} traces, and not over single traces.
For the deterministic input-output programs that we consider, and the specific safety hyperproperties we are interested in, the problem can be reduced to monitoring of trace properties.
In this paper, we present a simpler monitoring approach for safety hyperproperties of deterministic programs.
The approach involves transforming the given safety hyperproperty into a trace property, extracting a characteristic predicate for the given hyperproperty, and providing a parametric monitor taking such predicate as parameter.
For any hyperproperty in the considered subclass, we show how runtime verification monitors can be synthesised.
We have implemented our approach in the form of a parameterised monitor for the given class, and have applied it to a number of hyperproperties including data minimisation, non-interference, integrity and software doping. We show results concerning both offline and online monitoring.},
pdf = {formalise18-DataMin.pdf}
}
@techreport{PAS+18mdm,
author = {Srinivas Pinisetty and
Thibaud Antignac and
David Sands and
Gerardo Schneider},
title = {{Monitoring Data Minimisation}},
institution = {CoRR - arXiv.org},
number = {abs/1801.02484},
year = {2018},
url = {http://arxiv.org/abs/1801.02484},
archiveprefix = {arXiv},
eprint = {1801.02484},
timestamp = {Thu, 01 Feb 2018 19:52:26 +0100},
biburl = {https://dblp.org/rec/bib/journals/corr/abs-1801-02484}
}
@techreport{corrCPS14cnl,
author = {John J. Camilleri and
Gabriele Paganelli and
Gerardo Schneider},
title = {{A {CNL} for Contract-Oriented Diagrams}},
institution = {CoRR - arXiv.org},
number = {abs/1406.5691},
year = {2014},
url = {http://arxiv.org/abs/1406.5691},
archiveprefix = {arXiv},
eprint = {1406.5691},
timestamp = {Wed, 07 Jun 2017 14:40:19 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/CamilleriPS14}
}
@techreport{corrCGS16,
author = {John J. Camilleri and
Normunds Gruzitis and
Gerardo Schneider},
title = {{Extracting Formal Models from Normative Texts}},
institution = {CoRR - arXiv.org},
number = {abs/1607.01485},
year = {2016},
url = {http://arxiv.org/abs/1607.01485},
archiveprefix = {arXiv},
eprint = {1607.01485},
timestamp = {Wed, 07 Jun 2017 14:42:00 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/CamilleriGS16}
}
@techreport{corrASS16dm,
author = {Thibaud Antignac and
David Sands and
Gerardo Schneider},
title = {{Data Minimisation: A Language-Based Approach (Long Version)}},
institution = {CoRR - arXiv.org},
number = {abs/1611.05642},
year = {2016},
url = {http://arxiv.org/abs/1611.05642},
archiveprefix = {arXiv},
eprint = {1611.05642},
timestamp = {Wed, 07 Jun 2017 14:41:45 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/AntignacSS16}
}
@techreport{corrPSS17tek,
author = {Ra{\'{u}}l Pardo and
C{\'{e}}sar S{\'{a}}nchez and
Gerardo Schneider},
title = {{Timed Epistemic Knowledge Bases for Social Networks (Extended Version)}},
institution = {CoRR - arXiv.org},
number = {abs/1708.04070},
year = {2017},
url = {http://arxiv.org/abs/1708.04070},
archiveprefix = {arXiv},
eprint = {1708.04070},
timestamp = {Tue, 05 Sep 2017 10:03:46 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1708-04070}
}
@techreport{corr/CHS17wbt,
author = {John J. Camilleri and
Mohammad Reza Haghshenas and
Gerardo Schneider},
title = {{A Web-Based Tool for Analysing Normative Documents in English}},
institution = {CoRR - arXiv.org},
number = {abs/1707.03997},
year = {2017},
url = {http://arxiv.org/abs/1707.03997},
archiveprefix = {arXiv},
eprint = {1707.03997},
timestamp = {Sat, 05 Aug 2017 14:56:05 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/CamilleriHS17}
}
@inproceedings{ASS18pcm,
author = {Thibaud Antignac and Riccardo Scandariato and Gerardo Schneider},
title = {{Privacy Compliance via Model Transformations}},
booktitle = {International Workshop on Privacy Engineering (IWPE'18) at {IEEE} EuroS{\&}P Workshops},
pages = {120--126},
year = {2018},
opteditor = {},
optvolume = {},
optnumber = {},
optaddress = {London, UK},
optmonth = {27 April},
isbn = {978-1-5386-5445-3},
publisher = {{IEEE}},
url = {https://doi.org/10.1109/EuroSPW.2018.00024},
doi = {10.1109/EuroSPW.2018.00024},
pdf = {iwpe18.pdf},
abstract = {Due to the upcoming, more restrictive regulations (like the European GDPR), designing privacy preserving architectures for information systems is becoming a pressing concern for practitioners.
In particular, verifying that a design is compliant with the regulations might be a challenging task for engineers.
This work presents an approach based on model transformations, which guarantee that an architectural design encompasses regulation-oriented principles such as purpose limitation, or accountability of the data controller.
Our work improves the state of the art along two main dimensions.
The approach we propose (i) embeds privacy principles coming from regulations, thus helping to bridge the gap between the technical and the legal worlds, (ii) systematize the embedding of the privacy principles coming from regulations, thus enabling a constructive approach to privacy by design.
}
}
@inproceedings{PS17mcs,
author = {Ra{\'{u}}l Pardo and
Gerardo Schneider},
title = {{Model Checking Social Network Models}},
booktitle = {Eighth International Symposium on Games, Automata, Logics
and Formal Verification (GandALF'17)},
location = {Roma, Italy},
month = {September},
issn = {2075-2180},
pages = {238--252},
year = {2017},
url = {https://doi.org/10.4204/EPTCS.256.17},
doi = {10.4204/EPTCS.256.17},
series = {{EPTCS}},
volume = {256},
abstract = {A {\em social network service} is a platform to build social
relations among people sharing similar interests and activities.
The underlying structure of a social networks service is the
{\em social graph}, where nodes
represent users and the arcs represent the users' social
links and other kind of connections. One important concern in social networks
is {\em privacy}: what others are (not) allowed to {\em know} about
us. The ``logic of knowledge'' (\emph{epistemic logic}) is thus a
good
formalism to define, and reason about, privacy
policies.
In this paper we consider the problem of verifying knowledge properties
over {\em social network models} (SNMs), that is social graphs enriched with {\em knowledge bases} containing the information that the users know.
More concretely, our contributions are:
i) We prove that the model checking problem for
epistemic properties
over SNMs is decidable;
ii) We prove that a number of properties of knowledge that are sound w.r.t.~Kripke models are also sound w.r.t.~SNMs;
iii) We give a satisfaction-preserving encoding of SNMs into {\em canonical} Kripke models, and we also characterise which Kripke models may be translated into SNMs;
iv) We show that, for SNMs, the model checking problem is cheaper than the one based on standard Kripke models.
Finally, we have developed a proof-of-concept implementation of the model-checking algorithm for SNMs.},
pdf = {gandalf17.pdf}
}
@inproceedings{CRS18wbt,
author = {John J. Camilleri and Mohammad Reza Haghshenas and Gerardo Schneider},
title = {{A Web-Based Tool for Analysing Normative Documents in English}},
booktitle = {The 33rd ACM/SIGAPP Symposium On Applied Computing --Software Verification and Testing track (SAC-SVT'18)},
optseries = {SAC'18},
year = {2018},
isbn = {},
optlocation = {Pau, France},
pages = {1865--1872},
url = {http://doi.acm.org/10.1145/3167132.3167331},
doi = {10.1145/3167132.3167331},
publisher = {ACM},
abstract = {Our goal is to use formal methods to analyse normative documents written in English, such as privacy policies
and regulations.
This requires the combination of a number of different elements, including
information extraction from natural language,
formal languages for model representation,
and an interface for property specification and verification.
A number of components for performing these tasks have separately been developed:
a natural language extraction tool,
a suitable formalism for representing such documents,
an interface for building models in this formalism,
and methods for answering queries asked of a given model.
In this work, each of these concerns is brought together in a web-based tool, providing a single interface for analysing normative texts in English.
Through the use of a running example, we describe each component and demonstrate the workflow established by our tool.
},
pdf = {sac-svt18.pdf}
}
@inproceedings{LCC+17pvr,
author = {Luteberget, Bj{\o}rnar and Camilleri, John J. and Johansen, Christian and Schneider, Gerardo},
opteditor = {Cimatti, Alessandro and Sirjani, Marjan},
title = {{Participatory Verification of Railway Infrastructure by Representing Regulations in RailCNL}},
booktitle = {15th International Conference on Software Engineering and Formal Methods, (SEFM'17)},
year = {2017},
pages = {87--103},
volume = {10469},
series = {LNCS},
optaddress = {Trento, Italy},
optmonth = {4-8 September},
publisher = {Springer},
abstract = {Designs of railway infrastructure (tracks, signalling and control systems, etc.) need to comply with comprehensive sets of regulations describing safety requirements, engineering conventions, and design heuristics. We have previously worked on automating the verification of railway designs against such regulations, and integrated a verification tool based on Datalog reasoning into the CAD tools of railway engineers. This was used in a pilot project at Norconsult AS (formerly Anacon AS). In order to allow railway engineers with limited logic programming experience to participate in the verification process, in this work we introduce a controlled natural language, RailCNL, which is designed as a middle ground between informal regulations and Datalog code. Phrases in RailCNL correspond closely to those in the regulation texts, and can be translated automatically into the input language of the verifier. We demonstrate a prototype system which, upon detecting regulation violations, traces back from errors in the design through the CNL to the marked-up original text, allowing domain experts to examine the correctness of each translation step and better identify sources of errors. We also describe our design methodology, based on CNL best practices and previous experience with creating verification front-end languages.},
isbn = {978-3-319-66197-1},
doi = {10.1007/978-3-319-66197-1_6},
url = {https://doi.org/10.1007/978-3-319-66197-1_6},
pdf = {sefm2017.pdf}
}
@article{PBS17fpp,
author = {Ra\'ul Pardo and Musard Balliu and Gerardo Schneider},
title = {Formalising Privacy Policies in Social Networks},
journal = {Journal of Logical and Algebraic Methods in Programming},
volume = {90},
optnumber = {},
pages = {125--157},
month = {August},
year = {2017},
issn = {2352-2208},
doi = {https://doi.org/10.1016/j.jlamp.2017.02.008},
url = {http://www.sciencedirect.com/science/article/pii/S235222081730038X},
abstract = {Social Network Services (SNS) have changed the way people communicate, bringing many benefits but also new concerns. Privacy is one of them. We present a framework to write privacy policies for \{SNSs\} and to reason about such policies in the presence of events making the network evolve. The framework includes a model of SNSs, a logic to specify properties and to reason about the knowledge of the users (agents) of the SNS, and a formal language to write privacy policies. Agents are enhanced with a reasoning engine allowing the inference of knowledge from previously acquired knowledge. To describe the way \{SNSs\} may evolve, we provide operational semantics rules which are classified into four categories: epistemic, topological, policy, and hybrid, depending on whether the events under consideration change the knowledge of the SNS' users, the structure of the social graph, the privacy policies, or a combination of the above, respectively. We provide specific rules for describing Twitter's behaviour, and prove that it is privacy-preserving (i.e., that privacy is preserved under every possible event of the system). We also show how Twitter and Facebook are not privacy-preserving in the presence of additional natural privacy policies.},
pdf = {jlamp2017-privacy_policies.pdf}
}
@article{CS17man,
author = {John J. Camilleri and Gerardo Schneider},
title = {Modelling and Analysis of Normative Documents},
journal = {Journal of Logical and Algebraic Methods in Programming},
volume = {91},
optnumber = {},
pages = {33--59},
month = {October},
year = {2017},
issn = {2352-2208},
doi = {https://doi.org/10.1016/j.jlamp.2017.05.002},
url = {http://www.sciencedirect.com/science/article/pii/S2352220817300822},
abstract = {We are interested in using formal methods to analyse normative documents or contracts such as terms of use, privacy policies, and service agreements. We begin by modelling such documents in terms of obligations, permissions and prohibitions of agents over actions, restricted by timing constraints and including potential penalties resulting from the non-fulfilment of clauses. This is done using the C-O Diagram formalism, which we have extended syntactically and for which we have defined a new trace semantics. Models in this formalism can then be translated into networks of timed automata, and we have a complete working implementation of this translation. The network of automata is used as a specification of a normative document, making it amenable to verification against given properties. By applying this approach to a case study from a real-world contract, we show the kinds of analysis possible through both syntactic querying on the structure of the model, as well as verification of properties using Uppaal.},
pdf = {jlamp2017-normative_doc.pdf}
}
@inproceedings{AMS17sdv,
author = {Antignac, Thibaud and Mukelabai, Mukelabai and Schneider, Gerardo},
title = {{Specification, Design, and Verification of an Accountability-aware Surveillance Protocol}},
booktitle = {The 32nd ACM/SIGAPP Symposium On Applied Computing --Software Verification and Testing track (SAC-SVT'17)},
optseries = {SAC'17},
year = {2017},
isbn = {978-1-4503-4486-9},
location = {Marrakech, Morocco},
pages = {1372--1378},
url = {http://doi.acm.org/10.1145/3019612.3019826},
doi = {10.1145/3019612.3019826},
acmid = {3019826},
publisher = {ACM},
optkeywords = {accountability, formal verification, privacy, protocol},
abstract = {Though controversial, surveillance activities are more and more performed for security reasons. However, such activities are extremely privacy-intrusive. This is seen as a necessary side-effect to ensure the success of such operations. In this paper, we propose an accountability-aware protocol designed for surveillance purposes. It relies on a strong incentive for a surveillance organisation to register its activity to a data protection authority. We first elicit a list of accountability requirements, we provide an architecture showing the interaction of the different involved parties, and we propose an accountability-aware protocol which is formally specified in the applied pi calculus. We use the ProVerif tool to automatically verify that the protocol respects confidentiality, integrity and authentication properties.},
pdf = {sac-svt17.pdf}
}
@article{ACP+17vdc,
author = {Wolfgang Ahrendt and Mauricio Chimento and Gordon Pace and Gerardo Schneider},
title = {{Verifying Data- and Control-Oriented Properties Combining Static and Runtime Verification: Theory and Tools}},
journal = {Formal Methods in System Design},
year = {2017},
volume = {51},
number = {1},
pages = {200--265},
month = {August},
publisher = {Springer},
doi = {10.1007/s10703-017-0274-y},
isbn = {},
e-issn = {1572-8102},
issn = {0925-9856},
abstract = {Static verification techniques are used to analyse and prove properties about programs before they are executed. Many of these techniques work directly on the source code and are used to verify data-oriented properties over all possible executions. The analysis is necessarily an over-approximation as the real executions of the program are not available at analysis time. In contrast, runtime verification techniques have been extensively used for control-oriented properties, analysing the current execution path of the program in a fully automatic manner.
In this article, we present a novel approach in which data-oriented and control-oriented properties may be stated in a single formalism amenable to both static and dynamic verification techniques.
The specification language we present to achieve this that of ppDATEs, which enhances the control-oriented property language of DATEs,
with data-oriented pre/postconditions. For runtime verification of ppDATE specifications, the language is translated into a DATE. We give a formal semantics to ppDATEs, which we use to prove the correctness of our translation from ppDATEs to DATEs. We show how ppDATE specifications can be analysed using a combination of the deductive theorem prover KeY and the runtime verification tool LARVA. Verification is performed in two steps: KeY first partially proves the data-oriented part of the specification, simplifying the specification which is then passed on to LARVA to check at runtime for the remaining parts of the specification including the control-oriented aspects. We show the applicability of our approach on two case studies.
},
pdf = {fmsd2017.pdf}
}
@inproceedings{PPS17sps,
author = {Pablo Picazo-S\'anchez and Ra\'ul Pardo and Gerardo Schneider},
title = {{Secure Photo Sharing in Social Networks}},
booktitle = {IFIP Information Security \& Privacy Conference (IFIP SEC'17)},
pages = {79--92},
year = {2017},
opteditor = {Sabrina De Capitani di Vimercati and Fabio Martinelli},
volume = {502},
series = {IFIP Advances in Information and Communication Technology (AICT)},
address = {Rome, Italy},
optmonth = {29-31 May},
publisher = {Springer Science and Business Media},
doi = {10.1007/978-3-319-58469-0_6},
isbn = {978-3-319-58468-3},
e-issn = {},
issn = {18684238},
abstract = {Nowadays, in an ubiquitous world where everything is connected to the Internet and where social networks play an important role in our lives, security and privacy is a must. Billions of pictures are uploaded daily to social networks and, with them, parts of our private life are disclosed. In this work, we propose a practical solution for secure photo sharing on social network with independence of its architecture which can be either centralised or distributed. This solution solves the inconsistencies that appear in distributed social network as a consequence of treating photos and access policies separately. Specifically, we solve this open problem by attaching an access policy to the images and thus, each time a photo is re-shared, the access policy will travel together with the image.},
pdf = {ifip-sec2017-photo_sharing.pdf}
}
@inproceedings{TSS17dm,
author = {Thibaud Antignac and David Sands and Gerardo Schneider},
title = {{Data Minimisation: A Language-Based Approach}},
booktitle = {IFIP Information Security \& Privacy Conference (IFIP SEC'17)},
pages = {442--456},
year = {2017},
opteditor = {Sabrina De Capitani di Vimercati and Fabio Martinelli},
volume = {502},
series = {IFIP Advances in Information and Communication Technology (AICT)},
address = {Rome, Italy},
optmonth = {29-31 May},
publisher = {Springer Science and Business Media},
doi = {10.1007/978-3-319-58469-0_30},
isbn = {978-3-319-58468-3},
e-issn = {},
issn = {18684238},
abstract = {Data minimisation is a privacy-enhancing principle considered as one
of the pillars of personal data regulations. This principle dictates that personal
data collected should be no more than necessary for the specific purpose consented
by the user. In this paper we study data minimisation from a programming
language perspective. We assume that a given program embodies the purpose
of data collection, and define a data minimiser as a pre-processor for the input
which reduces the amount of information available to the program without compromising
its functionality. We give formal definitions, and provide a procedure
to synthesise a correct data minimiser for a given program.},
pdf = {ifip-sec17-data_min.pdf}
}
@article{APS+16ca,
author = {Shaun Azzopardi and Gordon J.~Pace and Fernando Schapachnik and Gerardo Schneider},
title = {{Contract Automata: An Operational View of Contracts Between Interactive Parties}},
journal = {Artificial Intelligence and Law},
year = {2016},
volume = {24},
number = {3},
pages = {203--243},
month = {September},
publisher = {Springer},
doi = {10.1007/s10506-016-9185-2},
isbn = {},
e-issn = {1572-8382},
issn = {0924-8463},
pdf = {arti2016.pdf},
abstract = {Deontic logic as a way of formally reasoning about norms, an important area in AI and law, has traditionally concerned itself about formalising provisions of general statutes.
Despite the long history of deontic logic, given the wide scope of the logic, it is difficult, if not impossible, to formalise all these notions in a single formalism, and there are still ongoing debates on appropriate semantics for deontic modalities in different contexts. In this paper, we restrict our attention to contracts between interactive parties, which are both general enough to be an interesting object of study but specific enough so as to narrow down the debates regarding the meaning of modalities, and present a formalism for reasoning about them.
}
}
@inproceedings{PKS+16sep,
author = {Ra\'ul Pardo and Ivana Kelly\'erov\'a and C\'esar S\'anchez and Gerardo Schneider},
title = {{Specification of Evolving Privacy Policies for Online Social Networks}},
booktitle = {23rd International Symposium on Temporal Representation and Reasoning (TIME'16)},
pages = {70--79},
year = {2016},
opteditor = {Curtis E. Dyreson and
Michael R. Hansen and
Luke Hunsberger},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {Lyngby, Denmark},
optmonth = {17-19 October},
publisher = {IEEE CPS},
abstract = {Online Social Networks are ubiquitous,bringing not only numerous new possibilities but also big threats and challenges. Privacy is one of them.
Most social networks today offer a limited set of (static) privacy settings,
not being able to express dynamic policies.
For instance, users might decide to protect their location during the night, or share information with difference audiences depending on their current position.
In this paper we introduce TFPPF, a formal framework to express, and reason about, dynamic (and recurrent) privacy policies that are activated or deactivated by context (events) or time.
Besides a formal policy language (TPPL), the framework includes a knowledge-based logic extended with (linear) temporal operators and a learning modality (TKBL). Policies, and formulae in the logic, are interpreted over (timed) traces representing the evolution of the social network. We prove that checking privacy policy conformance, and the model-checking problem for TKBL, are both decidable.},
doi = {10.1109/TIME.2016.15},
e-issn = {},
isbn = {978-1-5090-3825-1},
issn = {},
pdf = {time2016.pdf}
}
@inproceedings{PCP+16aba,
author = {Ra\'ul Pardo and Christian Colombo and Gordon Pace and Gerardo Schneider},
title = {{An Automata-based Approach to Evolving Privacy Policies for Social Networks}},
booktitle = {The 16th International Conference on Runtime Verification (RV'16)},
pages = {285--301},
year = {2016},
opteditor = {Yli{\`{e}}s Falcone and
C{\'{e}}sar S{\'{a}}nchez},
volume = {10012},
series = {LNCS},
optaddress = {Madrid, Spain},
optmonth = {23-30 September},
optorganization = {},
publisher = {Springer},
abstract = {Online Social Networks (OSNs) are ubiquitous, with more than 70\% of Internet users being active users of such networking services. This widespread use of OSNs brings with it big threats and challenges, privacy being one of them.
Most OSNs today offer a limited set of (static) privacy settings and do not allow for the definition, even less enforcement, of more dynamic privacy policies.
In this paper we are concerned with the specification and enforcement of dynamic (and recurrent) privacy policies that are activated or deactivated by context (events).
In particular, we present a novel formalism of policy automata, transition systems where privacy policies may be defined per state. We further propose an approach based on runtime verification techniques to define and enforce such policies. We provide a proof-of-concept implementation for the distributed social network Diaspora, using the runtime verification tool LARVA to synthesise enforcement monitors.},
doi = {10.1007/978-3-319-46982-9_18},
e-issn = {},
isbn = {978-3-319-46981-2},
issn = {},
pdf = {rv2016.pdf}
}
@inproceedings{APS16SE2,
author = {Wolfgang Ahrendt and Gordon Pace and Gerardo Schneider},
title = {{StaRVOOrS - Episode II, Strengthen and Distribute the Force}},
booktitle = {7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation -- ISoLA'16 (1); Track: Static and Runtime Verification: Competitors or Friends?},
pages = {402--415},
year = {2016},
opteditor = {Tiziana Margaria and Bernhard Steffen},
volume = {9952},
series = {LNCS},
optaddress = {Corfu, Greece},
month = {10-14 October},
optorganization = {},
publisher = {Springer},
abstract = {Static and runtime techniques for the verification of programs are complementary. They both have their advantages and disadvantages, and a natural question is whether they may be combined in such a way as to get the advantages of both without inheriting too much from their disadvantages. In a previous contribution to ISoLA'12, we have proposed StaRVOOrS (`Static and Runtime Verification of Object-Oriented Software'), a unified framework for combining static and runtime verification in order to check data- and control-oriented properties. Returning to ISoLA here, we briefly report on advances since then: a unified specification language for data- and control-oriented properties, a tool for combined static and runtime verification, and experiments. On that basis, we discuss two future research directions to strengthen the power, and broaden the scope, of combined static and runtime verification: (i) to use static analysis techniques to further optimise the runtime monitor, and (ii) to extend the framework to the distributed case.},
doi = {10.1007/978-3-319-47166-2_28},
isbn = {978-3-319-47165-5},
e-issn = {},
issn = {},
pdf = {ISoLA2016-starvoors.pdf}
}
@inproceedings{ASS16pac,
author = {Thibaud Antignac and Riccardo Scandariato and Gerardo Schneider},
title = {{A Privacy-Aware Conceptual Model for Handling Personal Data}},
booktitle = {7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation -- ISoLA'16 (1); Track: Privacy and Security Issues in Information Systems},
pages = {942--957},
year = {2016},
opteditor = {Tiziana Margaria and Bernhard Steffen},
volume = {9952},
series = {LNCS},
optaddress = {Corfu, Greece},
month = {10-14 October},
optorganization = {},
publisher = {Springer},
abstract = {Handling personal data adequately is one of the biggest challenges of our era.
Consequently, law and regulations are in the process of being released, like the European General Data Protection Regulation (GDPR), which attempt to deal with these challenging issue early on.
The core question motivating this work is how software developers can validate their technical design vis-a-vis the prescriptions of the privacy legislation.
In this paper, we outline the technical concepts related to privacy that need to be taken into consideration in a software design.
Second, we extend a popular design notation in order to support the privacy concepts illustrated in the previous point.
Third, we show how some of the prescriptions of the privacy legislation and standards may be related to a technical design that employs our enriched notation, which would facilitate reasoning about compliance.},
doi = {10.1007/978-3-319-47166-2_65},
isbn = {978-3-319-47165-5},
e-issn = {},
issn = {},
pdf = {isola2016_Security-DFD.pdf}
}
@inproceedings{Schneider16SEP,
author = {Gerardo Schneider},
title = {{On the Specification and Enforcement of Privacy-Preserving Contractual Agreements}},
booktitle = {7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation -- ISoLA'16 (2); Track: Runtime Verification and Enforcement, the (industrial) application perspective},
pages = {413--419},
year = {2016},
opteditor = {Tiziana Margaria and Bernhard Steffen},
volume = {9953},
series = {LNCS},
optaddress = {},
optnote = {10-14 October},
optorganization = {},
publisher = {Springer},
abstract = {We are here concerned with the enforcement at runtime of contractual agreements (e.g., Terms of Service) that respect users' privacy policies. We do not provide a technical solution to the problem but rather give an overview of a framework for such an enforcement, and briefly discuss related work and ideas on how to address part of the framework.},
doi = {10.1007/978-3-319-47169-3_34},
isbn = {978-3-319-47168-6},
e-issn = {},
issn = {},
pdf = {isola2016_RVE-contracts.pdf}
}
@inproceedings{PPS16REE,
author = {Gordon Pace and Ra\'ul Pardo and Gerardo Schneider},
title = {{On the Runtime Enforcement of Evolving Privacy Policies in Online Social Networks}},
booktitle = {7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation -- ISoLA'16 (2); Track: Runtime Verification and Enforcement, the (industrial) application perspective},
pages = {407--412},
year = {2016},
opteditor = {Tiziana Margaria and Bernhard Steffen},
volume = {9953},
series = {LNCS},
optaddress = {Corfu, Greece},
month = {10-14 October},
optorganization = {},
publisher = {Springer},
abstract = {Online Social Networks have increased the need to understand well and extend the expressiveness of privacy policies. In particular, the need to be able to define and enforce dynamic (and recurrent) policies that are activated or deactivated by context (events) or timeouts. We propose an automaton-based approach to define and enforce such policies using runtime verification techniques. In this paper we discuss how our proposed solution addresses this problem without focussing on concrete technical details.},
doi = {10.1007/978-3-319-47169-3_33},
isbn = {978-3-319-47168-6},
e-issn = {},
issn = {},
pdf = {isola16-RVE.pdf}
}
@inproceedings{CGS16efm,
abstract = {\emph{Normative texts} are documents based on the deontic notions of obligation, permission, and prohibition. Our goal is model such texts using the \codiag{} formalism, making them amenable to formal analysis, in particular verifying that a text satisfies properties concerning causality of actions and timing constraints. We present an experimental, semi-automatic aid to bridge the gap between a normative text and its formal representation. Our approach uses dependency trees combined with our own rules and heuristics for extracting the relevant components. The resulting tabular data can then be converted into a C-O Diagram.},
author = {John J.~Camilleri and Normunds Gruzitis and Gerardo Schneider},
booktitle = {21st International Conference on Applications of Natural Language to Information Systems (NLDB'16)},
pages = {403--408},
year = {2016},
doi = {10.1007/978-3-319-41754-7_40},
opteditor = {Elisabeth M{\'{e}}tais and
Farid Meziane and
Mohamad Saraee and
Vijayan Sugumaran and
Sunil Vadera},
month = {22-24 June},
publisher = {Springer},
series = {LNCS},
volume = {9612},
title = {{Extracting Formal Models from Normative Texts}}
}
@inproceedings{PSS15cpc,
abstract = {Defining and characterising conditional permissions has never been easy. Part of the problem, we believe, comes from the fact that there is not one but a whole family of possible deontic operators, all of them distinct and reasonable, that can be labelled as conditional permissions. In this article, rather than disputing the correct interpretation, we revisit a number of different interpretations the term has received in the literature, and propose appropriate formalisations for these interpretations within the context of contract automata.},
author = {Gordon J.~Pace and Fernando Schapachnik and Gerardo Schneider},
booktitle = {The 28th International Conference on Legal Knowledge and Information Systems (JURIX'15)},
doi = {10.3233/978-1-61499-609-5-61},
e-issn = {1879-8314},
isbn = {978-1-61499-608-8},
issn = {0922-6389},
optaddress = {Braga, Portugal},
optmonth = {December 10-11},
pages = {61--70},
pdf = {jurix2015.pdf},
publisher = {{IOS} Press},
series = {Frontiers in Artificial Intelligence and Applications},
title = {{Conditional Permissions in Contracts}},
volume = {279},
year = {2015},
bdsk-url-1 = {http://dx.doi.org/10.3233/978-1-61499-609-5-61}
}
@inproceedings{CAP+15stc,
abstract = {We present the tool StaRVOOrS (Static and Runtime Verification of Object-Oriented Software), which combines static and runtime verification (RV) of Java programs. The tool automates a framework which uses partial results extracted from static verification to optimise the runtime monitoring process. StaRVOOrs combines the deductive theorem prover KeY and the RV tool LARVA, and uses properties written using the ppDATE specification language which combines the control-flow property language DATE used in LARVA with Hoare triples assigned to states. We demonstrate the effectiveness of the tool by applying it to the electronic purse application Mondex.},
address = {Vienna, Austria},
author = {Jes\'us Mauricio Chimento and Wolfgang Ahrendt and Gordon Pace and Gerardo Schneider},
booktitle = {The 15th International Conference on Runtime Verification (RV'15)},
doi = {10.1007/978-3-319-23820-3_21},
opteditor = {Ezio Bartocci and Rupak Majumdar},
isbn = {978-3-319-23819-7},
issn = {0302-9743},
month = {September 22-25},
pages = {297--305},
pdf = {rv2015.pdf},
publisher = {Springer},
series = {LNCS},
title = {{STARVOORS: A Tool for Combined Static and Runtime Verification of Java}},
volume = {9333},
year = {2015},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-319-23820-3_21}
}
@inproceedings{ACP+15,
abstract = {Static verification techniques can verify properties across all executions of a program, but powerful judgements are hard to achieve automatically. In contrast, runtime verification enjoys full automation, but cannot judge future and alternative runs. In this paper we present a novel approach in which data-centric and control-oriented properties may be stated in a single formalism, amenable to both static and dynamic verification techniques. We develop and formalise a specification notation, ppDATE, extending the control-flow property language used in the runtime verification tool LARVA with pre/post-conditions and show how specifications written in this notation can be analysed both using the deductive theorem prover KeY and the runtime verification tool LARVA. Verification is performed in two steps: KeY first partially proves the data-oriented part of the specification, simplifying the specification which is then passed on to LARVA to check at runtime for the remaining parts of the specification including the control-centric aspects. We apply the approach to Mondex, an electronic purse application.},
address = {Oslo, Norway},
author = {Wolfgang Ahrendt and Mauricio Chimento and Gordon Pace and Gerardo Schneider},
booktitle = {Formal Methods (FM'15)},
doi = {10.1007/978-3-319-19249-9_8},
opteditor = {Nikolaj Bj{\o}rner and Frank D. de Boer},
isbn = {978-3-319-19248-2},
issn = {0302-9743},
month = {June 24-26},
pages = {108-125},
pdf = {fm2015.pdf},
publisher = {Springer},
series = {LNCS},
title = {A Specification Language for Static and Runtime Verification of Data and Control Properties},
volume = {9109},
year = {2015},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-319-19249-9_8}
}
@inproceedings{ESS15dpn,
abstract = {Differential privacy provides a way to get useful information about sensitive data without revealing much about any one individual. It enjoys many nice compositionality properties not shared by other approaches to privacy, including, in particular, robustness against side-knowledge.
Designing differentially private mechanisms from scratch can be a challenging task. One way to make it easier to construct new differential private mechanisms is to design a system which allows more complex mechanisms (programs) to be built from differentially private building blocks in principled way, so that the resulting programs are guaranteed to be differentially private by construction.
This paper is about a new accounting principle for building differentially private programs. It is based on a simple generalisation of classic differential privacy which we call Personalised Differential Privacy (PDP). In PDP each individual has its own personal privacy level. We describe ProPer, a interactive system for implementing PDP which maintains a privacy budget for each individual. When a primitive query is made on data derived from individuals, the provenance of the involved records determines how the privacy budget of an individual is affected: the number of records derived from Alice determines the multiplier for the privacy decrease in Alice's budget. This offers some advantages over previous systems, in particular its fine-grained character allows better utilisation of the privacy budget than mechanisms based purely on the concept of global sensitivity, and it applies naturally to the case of a live database where new individuals are added over time.
We provide a formal model of the ProPer approach, prove that it provides personalised differential privacy, and describe a prototype implementation based on McSherry's PINQ system.},
address = {Mumbai, India},
author = {Hamid Ebadi and David Sands and Gerardo Schneider},
booktitle = {Proceedings of the 42nd Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL}'15)},
doi = {10.1145/2676726.2677005},
isbn = {978-1-4503-3300-9},
month = {12-18 January},
opteditor = {Sriram K. Rajamani and David Walker},
optorganization = {Tata Institute of Fundamental Research},
pages = {69--81},
pdf = {popl2015.pdf},
publisher = {ACM},
title = {{Differential Privacy: Now it's Getting Personal}},
year = {2015},
bdsk-url-1 = {http://dx.doi.org/10.1145/2676726.2677005}
}
@inproceedings{CPS14cnl,
abstract = {We present a first step towards a framework for defining and manipulating normative documents or contracts described as Contract-Oriented (C-O) Diagrams.These diagrams provide a visual representation for such texts, giving the possibility to express a signatory's obligations, permissions and prohibitions, with or without timing constraints, as well as the penalties resulting from the non-fulfilment of a contract. This work presents a CNL for verbalising C-O Diagrams, a web-based tool allowing editing in this CNL, and another for visualising and manipulating the diagrams interactively. We then show how these proof-of-concept tools can be used by applying them to a small example.},
author = {John J.~Camilleri and Gabrielle Paganelli and Gerardo Schneider},
booktitle = {Fourth Workshop on Controlled Natural Language (CNL 2014)},
doi = {10.1007/978-3-319-10223-8_13},
isbn = {978-3-319-10222-1},
issn = {0302-9743},
optaddress = {Galway, Ireland},
opteditor = {Brian Davis and Kaarel Kaljurand and Tobias Kuhn},
pages = {135--146},
pdf = {cnl2014.pdf},
publisher = {Springer},
series = {LNCS},
title = {A CNL for Contract-Oriented Diagrams},
volume = {8625},
year = {2014},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-319-10223-8_13}
}
@inproceedings{PS14fpp,
abstract = {Social networks (SN) provide a great opportunity to help people
interact with each other in different ways depending on the kind of
relationship that links them. One of the aims of SN is to be
flexible in the way one shares information, being as permissive as
possible in how people communicate and disseminate
information. While preserving the spirit of SN, users would like to
be sure that their privacy is not compromised. One way to do so is
by providing users with means to define their own privacy policies
and give guarantees that they will be respected. In this paper we
present a privacy policy framework for SN, consisting of a formal
model of SN, a knowledge-based logic, and a formal privacy policy
language. The framework may be tailored by providing suitable
instantiations of the different relationships, the events, the
propositions representing what is to be known, and the additional
facts or rules a particular social network should satisfy. Besides,
models of Facebook and Twitter are instantiated in our formalism,
and we provide instantiations of a number of richer privacy
policies.},
author = {Ra\'ul Pardo and Gerardo Schneider},
booktitle = {12th International Conference on Software Engineering and Formal Methods (SEFM'14)},
doi = {10.1007/978-3-319-10431-7_30},
isbn = {978-3-319-10430-0},
issn = {0302-9743},
optaddress = {Grenoble, France},
opteditor = {D. Giannakopoulou and G. Sala\"um},
optmonth = {September 3-5},
pages = {378--392},
pdf = {sefm2014.pdf},
publisher = {Springer},
series = {LNCS},
title = {A Formal Privacy Policy Framework for Social Networks},
volume = {8702},
year = {2014},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-319-10431-7_30}
}
@inproceedings{CRS+13tfm,
abstract = {In this paper we report and reflect about the didactic principles
underlying our endeavour to write a book on `Formal Methods for
Software Engineering - Languages, Methods, Application Domains'',
and to teach its contents at international summer
schools`. Target audience
for the book are taught master students, possibly striving for a
career in industry, and doctoral students in their early years,
possibly in search of a suitable topic for their dissertation. We
outline ten principles underlying the design of the book, coin a
recommendation from each principle, and give appropriate examples.
We report about the feedback from participants to the schools and
lectures, and relate our principles to other pedagogical suggestions
for teaching Formal Methods.},
author = {Antonio Cerone and Markus Roggenbach and Holger Schlingloff and Gerardo Schneider and Siraj Shaikh},
booktitle = {Fun with Formal Methods Workshop},
month = {July},
pdf = {fwfm2013.pdf},
title = {Teaching Formal Methods for Software Engineering - Ten Principles},
year = {2013}
}
@proceedings{BPSsosym2013,
doi = {10.1007/s10270-014-0404-6},
editor = {Gilles Barthe and Alberto Pardo and Gerardo Schneider},
issn = {1619-1366},
month = {February},
number = {1},
publisher = {Springer},
series = {{Journal of Software and System Modeling (SoSyM)}},
title = {{Software Engineering and Formal Methods}},
volume = {14},
year = {2015},
bdsk-url-1 = {http://dx.doi.org/10.1007/s10270-014-0404-6}
}
@article{DCM+13svn,
author = {Gregorio D\'{i}az and M.~Emilia Cambronero and Enrique Mart\'{i}nez and Gerardo Schneider},
doi = {10.1109/TSE.2013.54},
issn = {0098-5589},
journal = {IEEE Transactions on Software Engineering},
number = {8},
pages = {795-817},
pdf = {tse2013.pdf},
title = {{Specification and Verification of Normative texts using C-O Diagrams}},
volume = {40},
year = {2014},
doi = {http://dx.doi.org/10.1109/TSE.2013.54},
abstract = {C-O Diagrams have been introduced as a means to have a more visual representation of normative texts and electronic contracts, where it is possible to represent the obligations, permissions and prohibitions of the different signatories, as well as the penalties resulting from non-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 information regarding the satisfaction and violation of clauses in order to represent different deontic modalities. As a proof of concept, we apply our approach to two different case studies, where the method presented here has successfully identified problems in the specification.}
}
@inproceedings{RS13moa,
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.},
address = {Malaga, Spain},
author = {Pavel Rabetski and Gerardo Schneider},
booktitle = {European Conference on Service-Oriented and Cloud Computing (ESOCC'13)},
doi = {10.1007/978-3-642-40651-5_19},
isbn = {978-3-642-40650-8},
issn = {0302-9743},
opteditor = {Kung-Kiu Lau and Winfried Lamersdorf and Ernesto Pimentel},
optmonth = {September 11-13},
pages = {227-241},
pdf = {esocc2013.pdf},
publisher = {Springer},
series = {LNCS},
title = {Migration of an on-premise application to the Cloud: Experience report},
volume = {8135},
year = {2013},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-40651-5_19}
}
@article{ACS13fca,
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.},
author = {Krasimir Angelov and John J.~Camilleri and Gerardo Schneider},
doi = {10.1016/j.jlap.2013.03.002},
issn = {1567-8326},
journal = {{Journal of Logic and Algebraic Programming}},
month = {July-October},
number = {5-7},
pages = {216-240},
pdf = {jlap13-CL_GF.pdf},
publisher = {Elsevier},
title = {A Framework for Conflict Analysis of Normative Texts Written in Controlled Natural Language},
volume = {82},
year = {2013},
bdsk-url-1 = {http://dx.doi.org/10.1016/j.jlap.2013.03.002}
}
@inproceedings{NST13atr,
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.},
address = {Rome, Italy},
author = {Robert Nagy and Gerardo Schneider and Aram Timofeitchik},
booktitle = {{19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13)}},
doi = {10.1007/978-3-642-36742-7_32},
isbn = {978-3-642-36741-0},
issn = {0302-9743},
opteditor = {N. Piterman and S. Smolka},
pages = {465-479},
pdf = {tacas2013.pdf},
publisher = {Springer},
series = {LNCS},
title = {Automatic Testing of Real-Time Graphics Systems},
volume = {7795},
year = {2013},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-36742-7_32}
}
@inproceedings{schneider12tfa,
address = {Bertinoro, Italy},
author = {Gerardo Schneider},
booktitle = {6th International Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS'12)},
issn = {2075-2180},
month = {19 September},
series = {EPTCS},
title = {Towards a Framework for Analyzing Normative Texts in Controlled Natural Language},
year = {2012}
}
@inproceedings{APS12uas,
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.},
address = {Heraclion, Crete},
author = {Wolfgang Ahrendt and Gordon J.~Pace and Gerardo Schneider},
booktitle = {5th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'12) - Part I},
doi = {10.1007/978-3-642-34026-0_24},
isbn = {978-3-642-34025-3},
issn = {0302-9743},
month = {15-18 October},
opteditor = {T.~Margaria and B.~Steffen and M.~Merten},
optnote = {Track: Runtime Verification: the application perspective},
pages = {312-326},
pdf = {isola12.pdf},
publisher = {Springer},
series = {LNCS},
title = {{A Unified Approach for Static and Runtime Verification: Framework and Applications}},
volume = {7609},
year = {2012},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-34026-0_24}
}
@proceedings{BS12flacos10,
doi = {10.1016/j.jlap.2011.12.003},
editor = {Antonio Brogi and Gerardo Schneider},
issn = {1567-8326},
month = {February},
number = {2},
publisher = {Elsevier},
series = {{Journal of Logic and Algebraic Programming}},
title = {{Special Section: Formal Languages and Analysis of Contract-Oriented Software (FLACOS'10)}},
volume = {81(2)},
year = {2012},
bdsk-url-1 = {http://dx.doi.org/10.1016/j.jlap.2011.12.003}
}
@article{HSS11rac,
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.},
author = {Hallstein Hansen and Gerardo Schneider and Martin Steffen},
doi = {10.1016/j.scico.2013.02.007},
issn = {0167-6423},
journal = {Science of Computer Programming (SCP)},
number = {12},
pages = {2511-2536},
pdf = {scp2013.pdf},
title = {Reachability analysis of complex planar hybrid systems},
volume = {78},
year = {2013},
bdsk-url-1 = {http://dx.doi.org/10.1016/j.scico.2013.02.007}
}
@techreport{HSS11racB,
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.},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Hallstein Hansen and Gerardo Schneider and Martin Steffen},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-374-5},
issn = {0806-3036},
month = {November},
number = {412},
pdf = {report-UiO-412.pdf},
title = {Reachability analysis of complex planar hybrid systems},
url = {http://urn.nb.no/URN:NBN:no-29825},
year = {2011},
bdsk-url-1 = {http://urn.nb.no/URN:NBN:no-29825}
}
@proceedings{BPSsefm11,
doi = {10.1007/978-3-642-24690-6},
editor = {Gilles Barthe and Alberto Pardo and Gerardo Schneider},
isbn = {978-3-642-24689-0},
issn = {0302-9743},
month = {November},
publisher = {Springer},
series = {{Lecture Notes in Computer Science}},
title = {{Software Engineering and Formal Methods}},
volume = {7041},
year = {2011},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-24690-6}
}
@inproceedings{MRS11fcs,
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.},
address = {M\'alaga, Spain},
author = {Seyed M. Montazeri and Nivir Roy and Gerardo Schneider},
booktitle = {5th International Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS'11)},
doi = {10.4204/EPTCS.68.6},
issn = {2075-2180},
month = {22-23 September},
pages = {55-69},
pdf = {flacos11-GFCL.pdf},
series = {EPTCS},
title = {{From Contracts in Structured English to CL Specifications}},
volume = {68},
year = {2011},
bdsk-url-1 = {http://dx.doi.org/10.4204/EPTCS.68.6}
}
@inproceedings{MCD+11tas,
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.},
address = {M\'alaga, Spain},
author = {Enrique Mart\'{i}nez and Mar\'{i}a E. Cambronero and Gregorio D\'{i}az and Gerardo Schneider},
booktitle = {5th International Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS'11)},
doi = {10.4204/EPTCS.68.3},
issn = {2075-2180},
month = {22-23 September},
pages = {7-21},
pdf = {flacos11-CO.pdf},
series = {EPTCS},
title = {{Timed Automata Semantics for Visual e-Contracts}},
volume = {68},
year = {2011},
bdsk-url-1 = {http://dx.doi.org/10.4204/EPTCS.68.3}
}
@proceedings{PS11flacos09,
doi = {10.1016/j.jlap.2011.04.001},
editor = {Gordon Pace and Gerardo Schneider},
issn = {1567-8326},
month = {April-July},
number = {3-5},
publisher = {Elsevier},
series = {{Journal of Logic and Algebraic Programming}},
title = {{Special Issue: Formal Languages and Analysis of Contract-Oriented Software}},
volume = {80(3-5)},
year = {2011},
bdsk-url-1 = {http://dx.doi.org/10.1016/j.jlap.2011.04.001}
}
@misc{BCG+11mrt,
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.},
author = {Ingram Bondin and Christian Colombo and Andrew Gauci and Gordon J. Pace and Gerardo Schneider},
note = {Submitted to IEEE Transactions on Software Engineering. Submitted Sep 2010; Revised Apr 2011},
optjournal = {Transactions on Software Engineering},
optpublisher = {IEEE},
title = {Monitoring Real-Time Properties with Overhead Guarantees},
year = {2011}
}
@article{PS12ddl,
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.},
author = {Cristian Prisacariu and Gerardo Schneider},
doi = {10.1016/j.jlap.2012.03.003},
issn = {1567-8326},
journal = {Journal of Logic and Algebraic Programming},
month = {May},
number = {4},
pages = {458-490},
pdf = {jlap2012.pdf},
publisher = {Elsevier},
title = {A Dynamic Deontic Logic for Complex Contracts},
volume = {81},
year = {2012},
bdsk-url-1 = {http://dx.doi.org/10.1016/j.jlap.2012.03.003}
}
@inproceedings{HSS11ran,
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.},
address = {Teheran, Iran},
author = {Hallstein A. Hansen and Gerardo Schneider and Martin Steffen},
booktitle = {Fourth International Conference on Fundamentals of Software Engineering (FSEN'11)},
doi = {10.1007/978-3-642-29320-7_14},
opteditor = {F. Arbab and M. Sirjani},
isbn = {978-3-642-29319-1},
issn = {0302-9743},
month = {20-22 April},
pages = {206-220},
pdf = {fsen2011.pdf},
publisher = {Springer},
series = {LNCS},
title = {{Reachability analysis of non-linear planar autonomous systems}},
volume = {7141},
year = {2012},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-29320-7_14}
}
@inproceedings{MS10avs,
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.},
author = {Enrique Martinez and Gerardo Schneider},
booktitle = {SPLC Workshops -- 1st International Workshop on Formal Methods in Software Product Line Engineering (FMSPLE'10)},
isbn = {978-1-86220-274-0},
month = {September},
optaddress = {Jeju Island, South Korea},
opturl = {http://dx.doi.org/},
pages = {75-82},
pdf = {FMSPLE10.pdf},
publisher = {Lancaster University},
title = {{Automated Analysis of Conflicts in Software Product Lines}},
volume = {2},
year = {2010}
}
@inproceedings{MCD+,
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.},
address = {Los Alamitos, USA},
author = {Enrique Martinez and Emilia Cambronero and Gregorio Diaz and Gerardo Schneider},
booktitle = {The 7th IEEE International Conference on Services Computing (IEEE SCC'10)},
doi = {10.1109/SCC.2010.32},
isbn = {978-0-7695-4126-6},
month = {July 5-10},
pages = {1--8},
pdf = {scc2010.pdf},
publisher = {IEEE Computer Society},
title = {{A Model for Visual Specification of e-Contracts}},
year = {2010},
bdsk-url-1 = {http://dx.doi.org/10.1109/SCC.2010.32}
}
@techreport{PS09flacos,
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Gordon J. Pace and Gerardo Schneider},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-345-1},
issn = {0806-3036},
month = {September},
note = {Editors},
number = {385},
pdf = {report-UiO-385.pdf},
title = {{FLACOS'09 Workshop Proceedings}},
year = {2009}
}
@techreport{CPS09rbr,
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.},
author = {Christian Colombo and Gordon Pace and Gerardo Schneider},
institution = {Department of Computer Science, University of Malta},
month = {December},
number = {CS2009-01},
pdf = {report-Malta-CS2009-01.pdf},
title = {Resource-bounded runtime verification of Java programs with real-time properties},
year = {2009}
}
@inproceedings{HS10rag,
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.},
address = {Sierre, Switzerland},
author = {Hallstein A. Hansen and Gerardo Schneider},
booktitle = {25th Annual ACM Symposium on Applied Computing --Software Verification and Testing track (SAC-SVT'10)},
doi = {10.1145/1774088.1774609},
isbn = {978-1-60558-639-7},
month = {March 22-26},
opteditor = {Sung Y. Shin and Sascha Ossowski and Michael Schumacher and Mathew J. Palakal and Chih-Cheng Hung},
pages = {2511-2516},
pdf = {sac10.pdf},
publisher = {ACM},
title = {{Reachability Analysis of GSPDIs: Theory, Optimization, and Implementation}},
year = {2010},
bdsk-url-1 = {http://dx.doi.org/10.1145/1774088.1774609}
}
@booklet{HS09ora,
address = {Lyngby, Denmark},
author = {Hallstein A. Hansen and Gerardo Schneider},
howpublished = {NWPT'09},
month = {October},
note = {Extended Abstract},
pdf = {nwpt09.pdf},
title = {{On the reachability analysis of planar, non-linear autonomous systems using hybrid systems}},
year = {2009}
}
@misc{BPS09cel,
author = {Gilles Barthe and Gordon J. Pace and Gerardo Schneider},
note = {In preparation},
title = {Contract Embedded Languages for Services},
year = {2009}
}
@inproceedings{FPS09ctc,
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.},
address = {Macao, China},
author = {Stephen Fenech and Gordon J. Pace and Gerardo Schneider},
booktitle = {7th International Symposium on Automated Technology for Verification and Analysis (ATVA'09)},
doi = {10.1007/978-3-642-04761-9_8},
isbn = {978-3-642-04760-2},
issn = {0302-9743},
month = {October},
opteditor = {Zhiming Liu and Anders P. Ravn},
pages = {90--96},
pdf = {atva09.pdf},
publisher = {Springer},
series = {LNCS},
title = {CLAN: A Tool for Contract Analysis and Conflict Discovery},
volume = {5799},
year = {2009},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-04761-9_8}
}
@article{AMP+12ldhs,
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.},
author = {Eugene Asarin and Venkatesh Mysore and Amir Pnueli and Gerardo Schneider},
doi = {10.1016/j.ic.2011.11.006},
issn = {0890-5401},
journal = {Information and Computation},
month = {January},
optnote = {Submitted Jun 2009, Revised Jun 2011, Accepted Nov 2011, Final Version Dec 2011},
pages = {138-159},
pdf = {infcomp2012.pdf},
publisher = {Elsevier},
title = {Low Dimensional Hybrid Systems - Decidable, Undecidable, Don't Know},
volume = {211},
year = {2012},
bdsk-url-1 = {http://dx.doi.org/10.1016/j.ic.2011.11.006}
}
@inproceedings{APSY02svt,
abstract = {We present SPeeDI, a tool for reachability analysis of Polygonal Hybrid Systems (SPDIs)},
address = {Copenhagen, Denmark},
author = {Eugene Asarin and Gordon Pace and Gerardo Schneider and Sergio Yovine},
booktitle = {Computer Aided Verification (CAV'02)},
doi = {10.1007/3-540-45657-0_28},
isbn = {978-3-642-03465-7},
issn = {0302-9743},
month = {July},
opteditor = {E. Brinksma and K.G. Larsen},
pages = {354--358},
pdf = {cav2002.pdf},
publisher = {Springer-Verlag},
series = {LNCS},
title = {{SPeeDI}: a verification tool for polygonal hybrid systems},
volume = {2404},
year = {2002},
bdsk-url-1 = {http://dx.doi.org/10.1007/3-540-45657-0_28}
}
@article{APSY08tcs,
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.},
author = {Eugene Asarin and Gordon Pace and Gerardo Schneider and Sergio Yovine},
doi = {10.1016/j.tcs.2007.09.025},
issn = {0304-3975},
journal = {Theoretical Computer Science},
month = {January},
number = {1},
pages = {1--26},
pdf = {tcs07-2.pdf},
publisher = {Elsevier},
title = {{Algorithmic Analysis of Polygonal Hybrid Systems. Part II: Phase Portrait and Tools}},
volume = {390},
year = {2008},
bdsk-url-1 = {http://dx.doi.org/10.1016/j.tcs.2007.09.025}
}
@inproceedings{AS02wgb,
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.},
address = {Brno, Czech Republic},
author = {Eugene Asarin and Gerardo Schneider},
booktitle = {13th International Conference on Concurrency Theory (CONCUR'02)},
doi = {10.1007/3-540-45694-5_14},
isbn = {3-540-44043-7},
issn = {0302-9743},
month = {August},
opteditor = {L. Brim and P. Jancar and M. Kretinsky and A. Kucera},
pages = {193--208},
pdf = {concur2002.pdf},
publisher = {Springer-Verlag},
series = {LNCS},
title = {Widening the boundary between decidable and undecidable hybrid systems},
volume = {2421},
year = {2002},
bdsk-url-1 = {http://dx.doi.org/10.1007/3-540-45694-5_14}
}
@inproceedings{ASY01drp,
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{\'e} 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.},
address = {Rome, Italy},
author = {Eugene Asarin and Gerardo Schneider and Sergio Yovine},
booktitle = {4th International Workshop on Hybrid Systems: Computation and Control (HSCC'01)},
doi = {10.1007/3-540-45351-2_11},
isbn = {3-540-41866-0},
issn = {0302-9743},
number = {2034},
opteditor = {M.D.~di Benedetto and A.~Sangiovanni-Vincentelli},
pages = {89--104},
pdf = {hs2001.pdf},
publisher = {Springer-Verlag},
series = {LNCS},
title = {On the decidability of the reachability problem for planar differential inclusions},
year = {2001},
bdsk-url-1 = {http://dx.doi.org/10.1007/3-540-45351-2_11}
}
@techreport{ASY01tr,
abstract = {This is an extended version of the HSCC'2001 paper.},
address = {Grenoble, France},
author = {Eugene Asarin and Gerardo Schneider and Sergio Yovine},
institution = {VERIMAG},
month = {January},
ps = {hs2001_ext.ps.gz},
title = {{On the decidability of the reachability problem for planar differential inclusions}},
year = {2001}
}
@inproceedings{ASY02tcp,
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.},
address = {Stanford, USA},
author = {Eugene Asarin and Gerardo Schneider and Sergio Yovine},
booktitle = {5th International Workshop on Hybrid Systems: Computation and Control (HSCC'02)},
doi = {10.1007/3-540-45873-5_7},
isbn = {3-540-43321-X},
issn = {0302-9743},
month = {March},
number = {2289},
opteditor = {C.J. Tomlin and M.R. Greenstreet},
pages = {49--61},
pdf = {hs2002.pdf},
publisher = {Springer-Verlag},
series = {LNCS},
title = {Towards Computing Phase Portraits of Polygonal Differential Inclusions},
year = {2002},
bdsk-url-1 = {http://dx.doi.org/10.1007/3-540-45873-5_7}
}
@article{ASY07tcs1,
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.
},
author = {Eugene Asarin and Gerardo Schneider and Sergio Yovine},
doi = {10.1016/j.tcs.2007.03.055},
issn = {0304-3975},
journal = {Theoretical Computer Science},
number = {1-2},
pages = {231--265},
pdf = {tcs07.pdf},
publisher = {Elsevier},
title = {{Algorithmic Analysis of Polygonal Hybrid Systems. Part I: Reachability}},
volume = {379},
year = {2007},
bdsk-url-1 = {http://dx.doi.org/10.1016/j.tcs.2007.03.055}
}
@techreport{BMS04bfs,
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.},
author = {Michael Baldamus and Richard Mayr and Gerardo Schneider},
institution = {Department of Information Technology, Uppsala University},
month = {January},
number = {2003-065},
pdf = {tech_rep_2003-065.pdf},
title = {A backward/forward strategy for verifying safety properties of infinite-state systems},
year = {2004}
}
@inproceedings{BPS05pam,
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.},
address = {Koblenz, Germany},
author = {Gilles Barthe and Mariela Pavlova and Gerardo Schneider.},
booktitle = {3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM'05)},
doi = {10.1109/SEFM.2005.34},
isbn = {0-7695-2435-4},
month = {September},
pages = {86--95},
pdf = {sefm2005.pdf},
publisher = {IEEE Computer Society},
title = {Precise analysis of memory consumption using program logics},
year = {2005},
bdsk-url-1 = {http://dx.doi.org/10.1109/SEFM.2005.34}
}
@inproceedings{CJPS05cmu,
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.},
address = {Newcastle Upon Tyne, UK},
author = {David Cachera and Thomas Jensen and David Pichardie and Gerardo Schneider},
booktitle = {Formal Methods (FM'05)},
doi = {10.1007/11526841_8},
isbn = {978-3-540-27882-5},
issn = {0302-9743},
month = {July},
pages = {91--106},
pdf = {fm2005.pdf},
publisher = {Springer-Verlag},
series = {LNCS},
title = {Certified memory usage analysis},
volume = {3582},
year = {2005},
bdsk-url-1 = {http://dx.doi.org/10.1007/11526841_8}
}
@inproceedings{CPS08lrt,
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.},
address = {L'Aquila, Italy},
author = {Christian Colombo and Gordon J. Pace and Gerardo Schneider},
booktitle = {{13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'08)}},
doi = {10.1007/978-3-642-03240-0_13},
isbn = {978-3-642-03239-4},
issn = {0302-9743},
month = {September},
pages = {135--149},
pdf = {fmics2008.pdf},
publisher = {Springer-Verlag},
series = {LNCS},
title = {Dynamic Event-Based Runtime Monitoring of Real-Time and Contextual Properties},
volume = {5596},
year = {2009},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-03240-0_13}
}
@inproceedings{CPS08sir,
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.},
address = {Budapest, Hungary},
author = {Christian Colombo and Gordon J. Pace and Gerardo Schneider},
booktitle = {The 7th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'09)},
doi = {10.1007/978-3-642-04368-0_10},
opteditor = {Joel Ouaknine and Frits Vaandrager},
isbn = {978-3-642-04367-3},
issn = {0302-9743},
note = {13-16 September},
pages = {103--117},
pdf = {formats2009.pdf},
publisher = {Springer},
series = {LNCS},
title = {Safe Runtime Verification of Real-Time Properties},
volume = {5813},
year = {2009},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-04368-0_10}
}
@inproceedings{CPS09ltr,
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.},
address = {Hanoi, Vietnam},
author = {Christian Colombo and Gordon J. Pace and Gerardo Schneider},
booktitle = {7th IEEE International Conference on Software Engineering and Formal Methods (SEFM'09)},
doi = {10.1109/SEFM.2009.13},
isbn = {978-0-7695-3870-9},
month = {23--27 November},
pages = {33--37},
pdf = {sefm2009.pdf},
publisher = {IEEE Computer Society},
title = {{LARVA --- Safer Monitoring of Real-Time Java Programs (Tool Paper)}},
year = {2009},
bdsk-url-1 = {http://dx.doi.org/10.1109/SEFM.2009.13}
}
@inproceedings{FOP+08bsc,
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.},
address = {York, UK},
author = {Stephen Fenech and Joseph Okika and Gordon J. Pace and Anders P. Ravn and Gerardo Schneider},
booktitle = {6th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA'09)},
doi = {10.1016/j.entcs.2009.09.027},
issn = {1571-0661},
month = {March},
number = {1},
pages = {39--55},
pdf = {fesca09-cocome.pdf},
series = {ENTCS},
title = {On the Specification of Full Contracts},
volume = {253},
year = {2009},
bdsk-url-1 = {http://dx.doi.org/10.1016/j.entcs.2009.09.027}
}
@booklet{FPS08cad,
address = {Tallinn, Estonia},
author = {Stephen Fenech and Gordon J. Pace and Gerardo Schneider},
howpublished = {NWPT'08},
month = {November 19--21},
note = {Extended Abstract},
pdf = {nwpt08.pdf},
title = {{Conflict Analysis of Deontic Contracts}},
year = {2008}
}
@inproceedings{FPS09acd,
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.},
address = {Kuala Lumpur, Malaysia},
author = {Stephen Fenech and Gordon J. Pace and Gerardo Schneider},
booktitle = {6th International Colloquium on Theoretical Aspects of Computing (ICTAC'09)},
doi = {10.1007/978-3-642-03466-4_13},
isbn = {978-3-642-03465-7},
issn = {0302-9743},
month = {August},
pages = {200--214},
pdf = {ictac09-contracts.pdf},
publisher = {Springer},
series = {LNCS},
title = {{Automatic Conflict Detection on Contracts}},
volume = {5684},
year = {2009},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-03466-4_13}
}
@incollection{GOR+07cos,
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.},
author = {Pablo Giambiagi and Olaf Owe and Anders P. Ravn and Gerardo Schneider},
booktitle = {{ERCIM News -- Special: The Future WEB}},
month = {January},
number = {72},
pages = {47--48},
pdf = {ercim08.pdf},
title = {Contract-Oriented Software Development for Internet Services},
url = {http://ercim-news.ercim.org/images/stories/EN72/EN72-web.pdf},
year = {2008},
bdsk-url-1 = {http://ercim-news.ercim.org/images/stories/EN72/EN72-web.pdf}
}
@techreport{GOSR06cbi,
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).},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Pablo Giambiagi and Olaf Owe and Anders P. Ravn and Gerardo Schneider},
institution = {Department of Informatics, University of Oslo},
issn = {0806-3036},
month = {January},
number = {333},
pdf = {report-UiO-333.pdf},
title = {Contract-based Internet Service Software Development: A Proposal},
year = {2006}
}
@inproceedings{GOSR06lbs,
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.},
address = {Set\'ubal, Portugal},
author = {Pablo Giambiagi and Olaf Owe and Anders P. Ravn and Gerardo Schneider},
booktitle = {International Conference on Software and Data Technologies (ICSOFT'06)},
isbn = {972-8865-69-4},
month = {September},
opteditor = {Joaquim Filipe and Boris Shishkov and Markus Helfert},
opturl = {http://dx.doi.org/},
pages = {339--344},
pdf = {icsoft2006.pdf},
publisher = {INSTICC Press},
title = {Language-based Support for Service Oriented Architectures: Future Directions},
year = {2006}
}
@inproceedings{GS05mca,
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.},
address = {Cali, Colombia},
author = {Pablo Giambiagi and Gerardo Schneider},
booktitle = {Proceedings of CLEI'05},
isbn = {958-670-426-2},
month = {October},
optpublisher = {Pontificia Universidad Javeriana Cali},
opturl = {http://dx.doi.org/},
pdf = {clei2005.pdf},
title = {Memory consumption analysis of Java smart cards},
year = {2005}
}
@booklet{GSV03nsi,
address = {Turku, Finland},
author = {Pablo Giambiagi and Gerardo Schneider and Frank D. Valencia},
howpublished = {NWPT'2003},
month = {October 29--31},
note = {Extended Abstract},
ps = {nwpt03_ccs.ps.gz},
title = {A note on scope and infinite behaviour in {CCS}-like calculi},
year = {2003}
}
@techreport{GSV04ecc,
abstract = {This an extended version of the FOSSACS 2004 paper.},
address = {Sweden},
author = {Pablo Giambiagi and Gerardo Schneider and Frank D. Valencia},
institution = {Department of Information Technology, Uppsala University},
month = {January},
number = {2004-002},
ps = {tec_rep_2004-002.ps.gz},
title = {{On the expressiveness of CCS-like calculi}},
year = {2004}
}
@inproceedings{GSV04eib,
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).},
address = {Barcelone, Spain},
author = {Pablo Giambiagi and Gerardo Schneider and Frank D. Valencia},
booktitle = {Foundations of Software Science and Computation Structures (FOSSACS'04)},
doi = {10.1007/978-3-540-24727-2_17},
isbn = {3-540-21298-1},
issn = {0302-9743},
month = {March},
pages = {226--240},
pdf = {fossacs2004.pdf},
publisher = {Springer-Verlag},
series = {LNCS},
title = {On the expressiveness of infinite behavior and name scoping in process calculi},
volume = {2987},
year = {2004},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-540-24727-2_17}
}
@inproceedings{HS07dpc,
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.},
address = {Manchester, UK},
author = {Johs H. Hammer and Gerardo Schneider},
booktitle = {3rd International Symposium on Information Assurance and Security (IAS'07)},
doi = {10.1109/IAS.2007.64},
isbn = {0-7695-2876-7},
month = {August},
pages = {337-342},
pdf = {ias2007.pdf},
publisher = {IEEE Computer Society Press},
title = {On the definition and policies of confidentiality},
year = {2007},
bdsk-url-1 = {http://dx.doi.org/10.1109/IAS.2007.64}
}
@inproceedings{HS09gta,
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.},
address = {Kuala Lumpur, Malaysia},
author = {Hallstein A. Hansen and Gerardo Schneider},
booktitle = {6th International Colloquium on Theoretical Aspects of Computing (ICTAC'09)},
doi = {10.1007/978-3-642-03466-4_23},
isbn = {978-3-642-03465-7},
issn = {0302-9743},
month = {August},
pages = {336--342},
pdf = {ictac09-GSPeeDI.pdf},
publisher = {Springer},
series = {LNCS},
title = {{GSPeeDI -- A Verification Tool for Generalized Polygonal Hybrid Systems}},
volume = {5684},
year = {2009},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-03466-4_23}
}
@techreport{JOS07nf,
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Einar B. Johnsen and Olaf Owe and Gerardo Schneider},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-324-9},
issn = {0806-3036},
month = {October},
note = {Editors},
number = {366},
pdf = {report-UiO-366.pdf},
title = {{NWPT'07/FLACOS'07 Workshop Proceedings}},
year = {2007}
}
@proceedings{JOS08nwpt,
doi = {10.1016/j.jlap.2009.06.001},
editor = {Einar B. Johnsen and Olaf Owe and Gerardo Schneider},
issn = {1567-8326},
month = {August/September},
number = {7},
publisher = {Elsevier},
series = {{Journal of Logic and Algebraic Programming}},
title = {{Special Issue: The 19th Nordic Workshop on Programming Theory (NWPT 2007)}},
volume = {78(7)},
year = {2009},
bdsk-url-1 = {http://dx.doi.org/10.1016/j.jlap.2009.06.001}
}
@inproceedings{JSO06rvc,
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.},
address = {Cluj-Napoca, Romania},
author = {Einar B. Johnsen and Gerardo Schneider and {\O}ystein Torget},
booktitle = {IEEE 2nd International Conference on Intelligent Computer Communication and Processing (ICCP'06)},
isbn = {978-973-662-233-5},
month = {September},
opturl = {http://dx.doi.org/},
pages = {161--168},
pdf = {iccp2006.pdf},
publisher = {U.T.Press},
title = {Runtime Validation of Communication Histories},
year = {2006}
}
@inproceedings{KPS08tbr,
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{\"u}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.},
address = {Seoul, South Korea},
author = {Marcel Kyas and Cristian Prisacariu and Gerardo Schneider},
booktitle = {{6th International Symposium on Automated Technology for Verification and Analysis (ATVA'08)}},
doi = {10.1007/978-3-540-88387-6_34},
isbn = {978-3-540-88386-9},
issn = {0302-9743},
month = {October},
pages = {397--407},
pdf = {atva2008.pdf},
publisher = {Springer-Verlag},
series = {LNCS},
title = {Run-time Monitoring of Electronic Contracts},
volume = {5311},
year = {2008},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-540-88387-6_34}
}
@inproceedings{OS08wos,
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.},
address = {York, UK},
author = {Olaf Owe and Gerardo Schneider},
booktitle = {6th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA'09)},
doi = {10.1016/j.entcs.2009.09.032},
issn = {1571-0661},
month = {March},
number = {1},
pages = {127--143},
pdf = {fesca09-wrappers.pdf},
series = {ENTCS},
title = {Wrap your Objects Safely},
volume = {253},
year = {2009},
bdsk-url-1 = {http://dx.doi.org/10.1016/j.entcs.2009.09.032}
}
@proceedings{OS09flacos,
doi = {10.1016/j.jlap.2009.02.012},
editor = {Olaf Owe and Gerardo Schneider},
issn = {1567-8326},
month = {May/June},
number = {5},
publisher = {Elsevier},
series = {{Journal of Logic and Algebraic Programming}},
title = {{Special Issue: Formal Languages and Analysis of Contract-Oriented Software (FLACOS'07)}},
volume = {78(5)},
year = {2009},
bdsk-url-1 = {http://dx.doi.org/10.1016/j.jlap.2009.02.012}
}
@proceedings{PS10flacos,
doi = {10.1016/j.jlap.2010.10.003},
editor = {Gordon Pace and Gerardo Schneider},
issn = {1567-8326},
month = {January},
number = {1},
publisher = {Elsevier},
series = {{Journal of Logic and Algebraic Programming}},
title = {{Special Issue: Formal Languages and Analysis of Contract-Oriented Software (FLACOS'08)}},
volume = {80(1)},
year = {2011},
bdsk-url-1 = {http://dx.doi.org/10.1016/j.jlap.2010.10.003}
}
@techreport{OSS07,
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.},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Olaf Owe and Gerardo Schneider and Martin Steffen},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-321-4},
issn = {0806-3036},
month = {August},
number = {363},
pdf = {report-UiO-363.pdf},
title = {Components, Objects, and Contracts},
year = {2007}
}
@inproceedings{OSS07coc,
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.},
address = {Dubrovnik, Croatia},
author = {Olaf Owe and Gerardo Schneider and Martin Steffen},
booktitle = {{6th Workshop on Specification And Verification of Component-Based Systems (SAVCBS'07)}},
doi = {10.1145/1292316.1292328},
isbn = {978-1-59593-721-6},
month = {September},
pages = {95--98},
pdf = {savcbs2007.pdf},
series = {ACM Digital Library},
title = {Components, Objects, and Contracts},
year = {2007},
bdsk-url-1 = {http://dx.doi.org/10.1145/1292316.1292328}
}
@inproceedings{OST07tix,
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.},
author = {Olaf Owe and Gerardo Schneider and Arild Torjusen},
booktitle = {NIK'07 proceedings},
isbn = {9788251922722},
opturl = {http://dx.doi.org/},
pages = {107--111},
pdf = {nik2007.pdf},
publisher = {Tapir Akademisk Forlag},
title = {{Towards integration of XML in the Creol object-oriented language}},
year = {2007}
}
@techreport{OST07tr,
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.},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Olaf Owe and Gerardo Schneider and Arild Torjusen},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-323-0},
issn = {0806-3036},
month = {October},
number = {365},
pdf = {report-UiO-365.pdf},
title = {{Towards integration of XML in the Creol object-oriented language}},
year = {2007}
}
@techreport{PPS07TRmcc,
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.},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Gordon Pace and Cristian Prisacariu and Gerardo Schneider},
institution = {Department of Informatics, University of Oslo},
issn = {0806-3036},
month = {August},
number = {362},
optisbn = {82-7368-320-6},
optissn = {0806-3036},
pdf = {report-UiO-362.pdf},
title = {Model Checking Contracts --A Case Study},
year = {2007}
}
@inproceedings{PPS07mcc,
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.},
address = {Tokyo, Japan},
author = {Gordon Pace and Cristian Prisacariu and Gerardo Schneider},
booktitle = {{5th International Symposium on Automated Technology for Verification and Analysis (ATVA'07)}},
doi = {10.1007/978-3-540-75596-8_8},
isbn = {978-3-540-75595-1},
issn = {0302-9743},
month = {October},
pages = {82--97},
pdf = {atva2007.pdf},
publisher = {Springer-Verlag},
series = {LNCS},
title = {Model Checking Contracts --A Case Study},
volume = {4762},
year = {2007},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-540-75596-8_8}
}
@inproceedings{PS04mcp,
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.},
address = {Venice, Italy},
author = {Gordon Pace and Gerardo Schneider},
booktitle = {5th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'04)},
doi = {10.1007/978-3-540-24622-0_11},
isbn = {978-3-540-20803-7},
issn = {0302-9743},
month = {December},
number = {2937},
pages = {110--121},
pdf = {vmcai2004.pdf},
publisher = {Springer Verlag},
series = {LNCS},
title = {Model Checking Polygonal Differential Inclusions Using Invariance Kernels},
year = {2003},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-540-24622-0_11}
}
@inproceedings{PS06,
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.},
address = {Paris, France},
author = {Gordon Pace and Gerardo Schneider},
booktitle = {4th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'06)},
doi = {10.1007/11867340_22},
isbn = {978-3-540-45026-9},
issn = {0302-9743},
month = {September},
pages = {306--321},
pdf = {formats2006.pdf},
publisher = {Springer-Verlag},
series = {LNCS},
title = {Static Analysis for State-Space Reduction of Polygonal Hybrid Systems},
volume = {4202},
year = {2006},
bdsk-url-1 = {http://dx.doi.org/10.1007/11867340_22}
}
@inproceedings{PS06cap,
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.},
address = {Tunis, Tunisia},
author = {Gordon J. Pace and Gerardo Schneider},
booktitle = {3rd International Colloquium on Theoretical Aspects of Computing (ICTAC'06)},
doi = {10.1007/11921240_12},
isbn = {3-540-48815-4},
issn = {0302-9743},
month = {November},
pages = {168--182},
pdf = {ictac2006.pdf},
publisher = {Springer-Verlag},
series = {LNCS},
title = {A Compositional Algorithm for Parallel Model Checking of Polygonal Hybrid Systems},
volume = {4281},
year = {2006},
bdsk-url-1 = {http://dx.doi.org/10.1007/11921240_12}
}
@booklet{PS06iph,
address = {Malta},
author = {Gordon Pace and Gerardo Schneider},
howpublished = {CSAW'06},
pdf = {csaw2006.pdf},
title = {Improving Polygonal Hybrid Systems Reachability Analysis through the use of the Phase Portrait},
year = {2006}
}
@techreport{PS06sas,
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.},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Gordon Pace and Gerardo Schneider},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-291-9},
issn = {0806-3036},
month = {April},
number = {336},
pdf = {report-UiO-336.pdf},
title = {Static Analysis of {SPDI}s for State-Space Reduction},
year = {2006}
}
@inproceedings{PS07cvp,
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.},
address = {Budapest, Hungary},
author = {Gordon Pace and Gerardo Schneider},
booktitle = {{14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08)}},
doi = {10.1007/978-3-540-78800-3_25},
isbn = {978-3-540-78799-0},
issn = {0302-9743},
month = {March},
pages = {341--345},
pdf = {tacas2008-tool.pdf},
publisher = {Springer-Verlag},
series = {LNCS},
title = {Computation and Visualisation of Phase Portraits for Model Checking SPDIs},
volume = {4963},
year = {2008},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-540-78800-3_25}
}
@inproceedings{PS07fle,
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.},
address = {Paphos, Cyprus},
author = {Prisacariu, Cristian and Schneider, Gerardo},
booktitle = {9th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS'07)},
doi = {10.1007/978-3-540-72952-5_11},
isbn = {978-3-540-72919-8},
issn = {0302-9743},
month = {June},
pages = {174--189},
pdf = {fmoods2007.pdf},
publisher = {Springer},
series = {LNCS},
title = {A Formal Language for Electronic Contracts},
volume = {4468},
year = {2007},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-540-72952-5_11}
}
@techreport{PS07tfd,
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.},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Cristian Prisacariu and Gerardo Schneider},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-305-2},
issn = {0806-3036},
month = {January},
number = {348},
pdf = {report-UiO-348.pdf},
title = {Towards a Formal Definition of Electronic Contracts},
year = {2007}
}
@booklet{PS07tmc,
address = {Oslo, Norway},
author = {Cristian Prisacariu and Gerardo Schneider},
howpublished = {{NWPT'07/FLACOS'07 Workshop Proceedings}},
month = {October 9--10},
note = {Extended Abstract},
pages = {104-106},
pdf = {flacos2007.pdf},
title = {Towards Model Checking Contracts},
year = {2007}
}
@techreport{PS07tr361,
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.},
address = {Oslo, Norway},
author = {Prisacariu, Cristian and Schneider, Gerardo},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-319-2},
issn = {0806-3036},
key = {TechRep},
keywords = {Electronic contracts, Kleene algebra, guarded rooted trees, concurrency, completeness},
month = {July},
note = {Updated March 2008},
number = {361},
pages = {64},
pdf = {report-UiO-361.pdf},
publisher = {Department of Informatics, University of Oslo},
title = {An {A}lgebraic {S}tructure for the {A}ction-{B}ased {C}ontract {L}anguage {CL} - theoretical results},
year = 2007
}
@techreport{PS08TRrgs,
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.},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Gordon Pace and Gerardo Schneider},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-331-1},
issn = {0806-3036},
month = {January},
number = {372},
pdf = {report-UiO-372.pdf},
title = {{Relaxing Goodness is Still Good for SPDIs}},
year = {2008}
}
@inproceedings{PS08csf,
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.},
address = {D\"useldorf, Germany},
author = {Gordon J. Pace and Gerardo Schneider},
booktitle = {{Integrated Formal Methods (iFM'09)}},
doi = {10.1007/978-3-642-00255-7_20},
isbn = {978-3-642-00254-0},
issn = {0302-9743},
month = {February},
pages = {292--306},
pdf = {ifm2009.pdf},
series = {LNCS},
title = {Challenges in the Specification of Full Contracts},
volume = {5423},
year = {2009},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-00255-7_20}
}
@techreport{PS08flacos,
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Gordon J. Pace and Gerardo Schneider},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-337-0},
issn = {0806-3036},
month = {October},
note = {Editors},
number = {377},
pdf = {report-UiO-377.pdf},
title = {{FLACOS'08 Workshop Proceedings}},
year = {2008}
}
@inproceedings{PS08rgs,
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.},
address = {Istanbul, Turkey},
author = {Gordon J. Pace and Gerardo Schneider},
booktitle = {{5th International Colloquium on Theoretical Aspects of Computing (ICTAC'08)}},
doi = {10.1007/978-3-540-85762-4_19},
isbn = {978-3-540-85761-7},
issn = {0302-9743},
month = {September},
opteditor = {J.S.Fitzgerald and A.E. Haxhausen and H. Yenigun},
pages = {274--289},
pdf = {ictac2008.pdf},
series = {LNCS},
title = {Relaxing Goodness is Still Good},
volume = {5160},
year = {2008},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-540-85762-4_19}
}
@techreport{PS08tr371,
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.},
address = {Oslo, Norway},
author = {Cristian Prisacariu and Gerardo Schneider},
isbn = {82-7368-330-3},
issn = {0806-3036},
month = {February},
number = {371},
pages = {68},
pdf = {report-UiO-371.pdf},
publisher = {Department of Informatics, University of Oslo},
title = {{CL: A Logic for Reasoning about Legal Contracts ---Semantics}},
year = 2008
}
@inproceedings{PS09asl,
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.},
address = {Barcelona, Spain},
author = {Cristian Prisacariu and Gerardo Schneider},
booktitle = {12th International Conference on Artificial Intelligence and Law (ICAIL'09)},
doi = {10.1145/1568234.1568262},
isbn = {978-1-60558-597-0},
month = {June},
pages = {218--219},
pdf = {icail09.pdf},
publisher = {ACM},
title = {Abstract Specification of Legal Contracts (Research Abstract)},
year = {2009},
bdsk-url-1 = {http://dx.doi.org/10.1145/1568234.1568262}
}
@inproceedings{PS09cl,
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.},
address = {Tokyo, Japan},
author = {Cristian Prisacariu and Gerardo Schneider},
booktitle = {16th Workshop on Logic, Language, Information and Computation (WOLLIC'09)},
doi = {10.1007/978-3-642-02261-6_27},
isbn = {978-3-642-02260-9},
issn = {0302-9743},
month = {June},
pages = {335--349},
pdf = {wollic09.pdf},
publisher = {Springer},
series = {LNCS},
title = {{CL: An Action-based Logic for Reasoning about Contracts}},
volume = {5514},
year = {2009},
bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-02261-6_27}
}
@booklet{SA96ill,
address = {Porto alegre, Brazil},
author = {Gerardo Schneider and Rafael Accorsi},
howpublished = {Primeiro Workshop sobre M\'etodos Formais e Qualidade de Software},
month = {July},
note = {(In Portuguese)},
pages = {15--42},
title = {Introduction to linear logic},
year = {1996}
}
@booklet{SR96spc,
address = {Bogot\'a, Colombia},
author = {Gerardo Schneider and Ant\^onio C. da Rocha Costa},
howpublished = {CLEI'96},
month = {June},
pages = {276--287},
title = {Sequential and parallel computation strategies on coherence spaces},
year = {1996}
}
@booklet{SR97cse,
address = {Brasilia, Brazil},
author = {Gerardo Schneider and Ant\^onio C. da Rocha Costa},
howpublished = {XXIV SEMISH},
month = {August},
pages = {423--434},
title = {Coherence space as event structure and concrete data structure},
year = {1997}
}
@booklet{ST95fpt,
address = {Curitiba, Brazil},
author = {Gerardo Schneider and Laira V. Toscani},
howpublished = {Anais do CNMAC},
month = {August},
note = {(Extended abstract, in Portuguese)},
pages = {150--154},
title = {Fixed point theory in Computer Science},
year = {1995}
}
@inproceedings{SX98tfs,
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.},
address = {Lyngby, Denmark},
author = {Gerardo Schneider and Xu Qiwen},
booktitle = {5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'98)},
doi = {10.1007/BFb0055355},
isbn = {978-3-540-65003-4},
issn = {0302-9743},
month = {September},
number = {1486},
opteditor = {Anders P. Ravn and Hans Rischel},
pages = {282--293},
pdf = {ftrtft98.pdf},
publisher = {Springer Verlag},
series = {LNCS},
title = {Towards a Formal Semantics of Verilog using Duration Calculus},
year = {1998},
bdsk-url-1 = {http://dx.doi.org/10.1007/BFb0055355}
}
@techreport{SX98tos,
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.},
address = {P.O.Box 3058, Macau},
author = {Gerardo Schneider and Xu Qiwen},
institution = {UNU/IIST},
month = {October},
number = {147},
ps = {report147.ps.gz},
title = {{Towards an Operational Semantics of Verilog}},
year = {1998}
}
@techreport{giambiagi98avs,
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.},
address = {P.O.Box 3058, Macau},
author = {Pablo Giambiagi and Gerardo Schneider},
institution = {UNU/IIST},
month = {February},
ps = {stari.ps.gz},
title = {{A Verilog specification of STARI}},
year = {1998}
}
@inproceedings{lafferriere00psr,
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.},
address = {Rio, Greece},
author = {Gerardo Lafferriere and George J. Pappas and Gerardo Schneider and Sergio Yovine},
booktitle = {Proceedings of 8th IEEE Mediterranean Conference on Control and Automation},
month = {July},
opturl = {http://dx.doi.org/},
pdf = {med2000.pdf},
title = {Parameter Synthesis in Robot Motion Planning Using Symbolic Reachability Computation},
year = {2000}
}
@phdthesis{schneider02,
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.},
address = {Grenoble, France},
author = {Gerardo Schneider},
month = {July},
pdf = {PhDthesis.pdf},
school = {VERIMAG -- UJF},
title = {Algorithmic Analysis of Polygonal Hybrid Systems},
year = {2002}
}
@booklet{schneider03cik,
address = {Turku, Finland},
author = {Gerardo Schneider},
howpublished = {NWPT'2003},
month = {October 29--31},
note = {Extended Abstract},
ps = {nwpt03_ik.ps.gz},
title = {Computing invariance kernels of polygonal hybrid systems},
year = {2003}
}
@techreport{schneider03ikp,
abstract = {This is the technical report corresponding to the journal paper "Computing invariance kernels of polygonal hybrid systems".},
author = {Gerardo Schneider},
institution = {Department of Information Technology, Uppsala University},
month = {August},
number = {2003-042},
ps = {tec_rep_2003-042.ps.gz},
title = {Invariance Kernels of Polygonal Differential Inclusions},
year = {2003}
}
@techreport{schneider04cba,
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.},
author = {Gerardo Schneider},
institution = {INRIA},
month = {December},
number = {RR-5440},
ps = {RR-5440.ps.gz},
title = {A constraint-based algorithm for analysing memory usage on Java cards},
year = {2004}
}
@booklet{schneider04mue,
address = {Uppsala, Sweden},
author = {Gerardo Schneider},
howpublished = {NWPT'2004},
month = {October 06--08},
note = {Extended Abstract},
ps = {nwpt04.ps.gz},
title = {Memory usage estimation for Java cards},
year = {2004}
}
@article{schneider04njc,
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.
},
author = {Gerardo Schneider},
issn = {1236-6064},
journal = {Nordic Journal of Computing},
number = {2},
opturl = {http://dx.doi.org/},
pages = {194--210},
pdf = {njc.pdf},
title = {Computing Invariance Kernels of Polygonal Hybrid Systems},
volume = {11},
year = {2004}
}
@techreport{schneider05tcp,
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.},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Gerardo Schneider},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-286-2},
issn = {0806-3036},
month = {March},
number = {331},
pdf = {report-UiO-331.pdf},
title = {Towards Computing Phase Portrait Objects of Polygonal Hybrid Systems on Surfaces},
year = {2005}
}
@techreport{schneider07drp,
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.},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Gerardo Schneider},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-317-6},
issn = {0806-3036},
month = {June},
number = {359},
pdf = {report-UiO-359.pdf},
title = {On the Decidability of the Reachability Problem for {GSPDIs}},
year = {2007}
}
@inproceedings{schneider08rag,
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.},
address = {Fortaleza, Brazil},
author = {Gerardo Schneider},
booktitle = {23rd Annual ACM Symposium on Applied Computing --Software Verification track (SAC-SV'08)},
doi = {10.1145/1363686.1363773},
isbn = {978-1-59593-753-7},
month = {March},
pages = {327--332},
pdf = {sac-sv2008.pdf},
publisher = {ACM},
title = {Reachability Analysis of {Generalized Polygonal Hybrid Systems}},
year = {2008},
bdsk-url-1 = {http://dx.doi.org/10.1145/1363686.1363773}
}
@techreport{schneider92uia,
address = {Concepci\'on del Uruguay, Argentina},
author = {Gerardo Schneider},
institution = {{Dissertation for Engineering Degree. Facultad Regional Concepci\'on del Uruguay - UTN}},
month = {December},
note = {(In Spanish)},
pages = {91},
title = {{Using induction for algorithm design}},
year = {1992}
}
@techreport{schneider94asl,
address = {Porto Alegre, Brazil},
author = {Gerardo Schneider},
institution = {CPGCC da UFRGS},
month = {July},
note = {(In Portuguese)},
pages = {44},
title = {{An algebraic specification language}},
year = {1994}
}
@techreport{schneider95fpt,
address = {Porto Alegre, Brazil},
author = {Gerardo Schneider},
institution = {CPGCC da UFRGS},
month = {January},
note = {(In Portuguese)},
pages = {68},
title = {{Fixed point theory in Computer Science}},
year = {1995}
}
@mastersthesis{schneider96,
address = {Porto Alegre, Brazil},
author = {Gerardo Schneider},
month = {March},
note = {(In Portuguese)},
pages = {144},
ps = {tesis.ps.gz},
school = {CPGCC -- UFRGS},
title = {Sequential and Parallel Computation Strategies on Coherence Spaces},
year = {1996}
}
@techreport{schneider98tfs,
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.},
address = {P.O.Box 3058, Macau},
author = {Gerardo Schneider and Xu Qiwen},
institution = {UNU/IIST},
month = {February},
number = {133},
ps = {report133.ps.gz},
title = {{Towards a Formal Semantics of Verilog using Duration Calculus}},
year = {1998}
}
This file was generated by bibtex2html 1.97.