5 Search Results for "Talcott, Carolyn"

Document
DOI: 10.4230/DagRep.9.11.97
Composing Model-Based Analysis Tools (Dagstuhl Seminar 19481)

Authors: Francisco Durán, Robert Heinrich, Diego Pérez-Palacín, Carolyn L. Talcott, and Steffen Zschaler

Published in: Dagstuhl Reports, Volume 9, Issue 11 (2020)

Abstract
This report documents the program and the outcomes of the Dagstuhl Seminar 19481 "Composing Model-Based Analysis Tools". The key objective of the seminar was to provide more flexibility in model-driven engineering by bringing together representatives from industry and researchers in the formal methods and software engineering communities to establishing the foundations for a common understanding on the modularity and composition of modeling languages and model-based analyses.
Cite as

Francisco Durán, Robert Heinrich, Diego Pérez-Palacín, Carolyn L. Talcott, and Steffen Zschaler. Composing Model-Based Analysis Tools (Dagstuhl Seminar 19481). In Dagstuhl Reports, Volume 9, Issue 11, pp. 97-116, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{duran_et_al:DagRep.9.11.97,
  author =	{Dur\'{a}n, Francisco and Heinrich, Robert and P\'{e}rez-Palac{\'\i}n, Diego and Talcott, Carolyn L. and Zschaler, Steffen},
  title =	{{Composing Model-Based Analysis Tools (Dagstuhl Seminar 19481)}},
  pages =	{97--116},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2020},
  volume =	{9},
  number =	{11},
  editor =	{Dur\'{a}n, Francisco and Heinrich, Robert and P\'{e}rez-Palac{\'\i}n, Diego and Talcott, Carolyn L. and Zschaler, Steffen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.9.11.97},
  URN =		{urn:nbn:de:0030-drops-119853},
  doi =		{10.4230/DagRep.9.11.97},
  annote =	{Keywords: Modelling, Simulation, Semantics, Formal Methods, Software Engineering}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.RTA.2015.22
Executable Formal Models in Rewriting Logic (Invited Talk)

Authors: Carolyn Talcott

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Abstract
Formal executable models provide a means to gain insights into the behavior of complex distributed systems. Ideas can be prototyped and assurance gained by carrying out analyses at different levels of fidelity: searching for desirable or undesirable behaviors, determining effects of perturbing the system, and eventually investing effort to carry out formal proofs of key properties. This modeling approach applies to a wide range of systems, including a variety of protocols and networked cyber-physical systems. It is also emerging as an important tool in understanding many different aspects of biological systems. Rewriting logic (RWL) is a formalism that is well-suited to developing and working with formal executable models. In RWL term rewriting is used to represent both structure (equational properties and functions) and transformation / behavior. Logics and inference systems can be naturally represented in RWL, as can the structure and behavior of distributed systems both engineered and natural. Maude is a high performance realization of Rewriting Logic. Maude specifications are naturally executable and the Maude environment provides a variety analysis tools to reason about properties of models. These include reachability analysis, symbolic execution (narrowing), and model-checking. In addition, Maude is reflective. This provides a powerful mechanism for extension. The talk will present a sampling of executable specifications using Maude and its extensions.
Cite as

Carolyn Talcott. Executable Formal Models in Rewriting Logic (Invited Talk). In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, p. 22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{talcott:LIPIcs.RTA.2015.22,
  author =	{Talcott, Carolyn},
  title =	{{Executable Formal Models in Rewriting Logic}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{22--22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.22},
  URN =		{urn:nbn:de:0030-drops-51861},
  doi =		{10.4230/LIPIcs.RTA.2015.22},
  annote =	{Keywords: Executable model, formal analysis, rewriting logic}
}
Document
DOI: 10.4230/LIPIcs.RTA.2012.305
A Rewriting Framework for Activities Subject to Regulations

Authors: Max Kanovich, Tajana Ban Kirigin, Vivek Nigam, Andre Scedrov, Carolyn Talcott, and Ranko Perovic

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
Activities such as clinical investigations or financial processes are subject to regulations to ensure quality of results and avoid negative consequences. Regulations may be imposed by multiple governmental agencies as well as by institutional policies and protocols. Due to the complexity of both regulations and activities there is great potential for violation due to human error, misunderstanding, or even intent. Executable formal models of regulations, protocols, and activities can form the foundation for automated assistants to aid planning, monitoring, and compliance checking. We propose a model based on multiset rewriting where time is discrete and is specified by timestamps attached to facts. Actions, as well as initial, goal and critical states may be constrained by means of relative time constraints. Moreover, actions may have non-deterministic effects, that is, they may have different outcomes whenever applied. We demonstrate how specifications in our model can be straightforwardly mapped to the rewriting logic language Maude, and how one can use existing techniques to improve performance. Finally, we also determine the complexity of the plan compliance problem, that is, finding a plan that leads from an initial state to a desired goal state without reaching any undesired critical state. We consider all actions to be balanced, that is, their pre and post-conditions have the same number of facts. Under this assumption on actions, we show that the plan compliance problem is PSPACE-complete when all actions have only deterministic effects and is EXPTIME-complete when actions may have non-deterministic effects.
Cite as

Max Kanovich, Tajana Ban Kirigin, Vivek Nigam, Andre Scedrov, Carolyn Talcott, and Ranko Perovic. A Rewriting Framework for Activities Subject to Regulations. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 305-322, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{kanovich_et_al:LIPIcs.RTA.2012.305,
  author =	{Kanovich, Max and Ban Kirigin, Tajana and Nigam, Vivek and Scedrov, Andre and Talcott, Carolyn and Perovic, Ranko},
  title =	{{A Rewriting Framework for Activities Subject to Regulations}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{305--322},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.305},
  URN =		{urn:nbn:de:0030-drops-35000},
  doi =		{10.4230/LIPIcs.RTA.2012.305},
  annote =	{Keywords: Multiset Rewrite Systems, Collaborative Systems, Applications of Rewrite Systems, Clinical Investigations, Maude}
}
Document
DOI: 10.4230/LIPIcs.RTA.2011.31
Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6

Authors: Francisco Duran, Steven Eker, Santiago Escobar, Jose Meseguer, and Carolyn Talcott

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

Abstract
This paper introduces some novel features of Maude 2.6 focusing on the variants of a term. Given an equational theory (Sigma,Ax cup E), the E,Ax-variants of a term t are understood as the set of all pairs consisting of a substitution sigma and the E,Ax-canonical form of t sigma. The equational theory (Ax cup E ) has the finite variant property if there is a finite set of most general variants. We have added support in Maude 2.6 for: (i) order-sorted unification modulo associativity, commutativity and identity, (ii) variant generation, (iii) order-sorted unification modulo finite variant theories, and (iv) narrowing-based symbolic reachability modulo finite variant theories. We also explain how these features have a number of interesting applications in areas such as unification theory, cryptographic protocol verification, business processes, and proofs of termination, confluence and coherence.
Cite as

Francisco Duran, Steven Eker, Santiago Escobar, Jose Meseguer, and Carolyn Talcott. Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 31-40, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{duran_et_al:LIPIcs.RTA.2011.31,
  author =	{Duran, Francisco and Eker, Steven and Escobar, Santiago and Meseguer, Jose and Talcott, Carolyn},
  title =	{{Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{31--40},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.31},
  URN =		{urn:nbn:de:0030-drops-31211},
  doi =		{10.4230/LIPIcs.RTA.2011.31},
  annote =	{Keywords: Rewriting logic, narrowing, unification, variants}
}
Document
DOI: 10.4230/DagSemProc.05081.7
Practical Techniques for Language Design and Prototyping

Authors: Mark-Oliver Stehr and Carolyn Talcott L.

Published in: Dagstuhl Seminar Proceedings, Volume 5081, Foundations of Global Computing (2006)

Abstract
Global computing involves the interplay of a vast variety of languages, but practially useful foundations for language specification and prototyping at the semantic level are lacking. In this talk we present a systematic approach consisting of three techniques: 1. A generic calculus of explicit substitutions with names (called CINNI) that allows us give a first-order representation of syntax to uniformly deal with all binding aspects. 2. An executable representation of Felleisen-style operational semantics in terms of first-order rewrite rules. 3. A logical framework, namely rewriting logic, that allows us to express (1) and (2) and, in addition, language aspects such as concurrency and non-determinism. We illustrate the use of these techniques in two applications: 1. A formal specification and analysis of PLAN, a Packet Language for Active Networks, that has been developed in the Switchware project at UPenn. This work was conducted in the scope of the DARPA Active Network Program. 2. The development of CIAO, a Calculus of Imperative Active Objects, a core language for concurrent object-oriented programming. It is especially designed to allow a the representation of practically relevant sublanguages of common object-oriented languages such as Java, C#, and C++. This second application is subject of ongoing work.
Cite as

Mark-Oliver Stehr and Carolyn Talcott L.. Practical Techniques for Language Design and Prototyping. In Foundations of Global Computing. Dagstuhl Seminar Proceedings, Volume 5081, pp. 1-38, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{stehr_et_al:DagSemProc.05081.7,
  author =	{Stehr, Mark-Oliver and Talcott L., Carolyn},
  title =	{{Practical Techniques for Language Design and Prototyping}},
  booktitle =	{Foundations of Global Computing},
  pages =	{1--38},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5081},
  editor =	{Jos\'{e} Luiz Fiadeiro and Ugo Montanari and Martin Wirsing},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05081.7},
  URN =		{urn:nbn:de:0030-drops-3006},
  doi =		{10.4230/DagSemProc.05081.7},
  annote =	{Keywords: Rewriting logic, explicit substitutions, operational semantics, active networks, active objects}
}
  • Refine by Author
  • 3 Talcott, Carolyn
  • 1 Ban Kirigin, Tajana
  • 1 Duran, Francisco
  • 1 Durán, Francisco
  • 1 Eker, Steven
  • Show More...

  • Refine by Classification
  • 1 General and reference → General literature

  • Refine by Keyword
  • 2 Rewriting logic
  • 1 Applications of Rewrite Systems
  • 1 Clinical Investigations
  • 1 Collaborative Systems
  • 1 Executable model
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 1 2006
  • 1 2011
  • 1 2012
  • 1 2015
  • 1 2020

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact