| Maude: A Wide Spectrum Language for Secure Active Networks |
AUG 2002 |
30 pages |
| Authors:
Jose Meseguer; Carolyn Talcott; SRI INTERNATIONAL MENLO PARK CA COMPUTER SCIENCE LAB
|
 | Modeling and formally analyzing active network systems and protocols is quite challenging, due to their highly dynamic nature and the need, for new network models. In this report, we propose a wide-spectrum methodology using executable rewriting logic specifications to address this challenge. We also show how, using the Maude rewriting logic language and tools, active network systems, languages, and protocols can be formally specified and analyzed using a wide range ... |
|
| Object-Oriented Design and Specification |
31 DEC 94 |
14 pages |
| Authors:
Jose Meseguer; SRI INTERNATIONAL MENLO PARK CA
|
| This final report summarizes the research performed for the Office of Naval Research under Contract N00014-90-C-0086 on the topic "Object-Oriented Design and Specification." The project began on 1 January 1990 and ended on 31 December 1994. Dr. Jose Meseguer was the project leader. Drs. Patrick Lincoln, and Narciso Martf-Oliet and Mr. Timothy Winkler also worked on the project. Early in the project, an important breakthrough took place with the discovery ... |
|
| Logics and Models for Concurrently and Type Theory |
12 OCT 92 |
|
| Authors:
Jose Meseguer; SRI INTERNATIONAL MENLO PARK CA
|
 | This reporting period is the last period of the project. During this last period substantial progress had been made in the following areas: (1) Linear logic and concurrency; (2) Rewriting logic and concurrency; and (3) Concurrency models. |
|
| Object-Oriented Design and Specification |
12 OCT 92 |
|
| Authors:
Jose Meseguer; SRI INTERNATIONAL MENLO PARK CA
|
| We have made substantial progress in the following areas: (1) The OBJ language; (2) Concurrent object-oriented programming and the Maude language; (3) Massive parallelism for declarative languages; and (4) Computability of algebraic data types. |
|
| Logics and Models for Concurrency and Type Theory |
16 JUN 92 |
15 pages |
| Authors:
Jose Meseguer; SRI INTERNATIONAL MENLO PARK CA
|
| The goal was to contribute useful new concepts and results in two very active areas of research within semantics of computation, namely concurrency and type theory. The technical method of approach used logic and category theory and aimed at a conceptual unification of concurrency and constructive type theory. Section 2 summarizes the accomplishments attained under this contract and explains the specific ways in which the research goals were met. Several ... |
|
| The Rewrite Rule Machine Project |
01 MAY 89 |
|
| Authors:
Joseph A. Goguen; Jose Meseguer; Sany Leinwand; Timothy Winkler; Hitoshi Aida; SRI INTERNATIONAL MENLO PARK CA
|
| Current generation parallel machines are typically either coarse- grain or fine-grain. Each design has certain limits, either in the amount of parallelism that it can effectively exploit, or else in the types of problem for which it is suitable. For example, only very homogeneous computations can make efficient use of today's fine-grained machines. However, many complex computations are locally homogeneous, but not globally homogeneous. The Rewrite Rule Machine (RRM) resolves ... |
|
| General Logics |
89 |
|
| Authors:
Jose Meseguer; SRI INTERNATIONAL MENLO PARK CA
|
| The connections between logic and computer science are growing rapidly and are becoming deeper. Besides theorem proving, logic programming, and program specification and verification, other areas showing a fascinating mutual interaction with logic include type theory, concurrency, artificial intelligence, complexity theory, databases, operational semantics, and compiler techniques. The concepts presented in this paper are motivated by the need to understand and relate the many different logics currently being used in ... |
|
| Rewrite Rule Machine |
JUL 86 |
|
| Authors:
Joseph Goguen; Claude Kirchner; Sany Leinwand; Jose Meseguer; Timothy Winkler; SRI INTERNATIONAL MENLO PARK CA
|
| Perhaps the most significant accomplishment of the Rewrite Rule Machine (RRM) project so far has been to explore the hardware and software implications of a novel model of computation, concurrent tree rewriting. This model serves as a bridge between easily programmed Ultra High Level Languages (UHLLs), featuring implicit concurrency, and advanced architectural designs having unprecedented performance (thousands of MIPS). Additional accomplishments include: (1) construction of a (high level) instrumented simulator ... |
|
| A Rewrite Rule Machine. Models of Computation for the Rewrite Rule Machine |
JUL 86 |
|
| Authors:
Joseph Goguen; Claude Kirchner; Jose Meseguer; SRI INTERNATIONAL MENLO PARK CA COMPUTER SCIENCE LAB
|
| A new model of computation, concurrent tree rewriting, is proposed as a bridge easily programmed Ultra High Level Languages (UHLLs) featuring implicit concurrency, and an advanced parallel architecture of unprecedented performance, the Rewrite Rule Machine (RRM) architecture. At the highest level of abstraction, computation is understood as rewriting a tree at multiple sites concurrently. Less abstractly, such a (possibly very large) tree can be partitioned into fragments that are assigned ... |
|
| OBJ-1, A Study in Executable Algebraic Formal Specification |
JUL 1981 |
|
| Authors:
Joseph A. Goguen; Jose Meseguer; SRI INTERNATIONAL MENLO PARK CA COMPUTER SCIENCE LAB
|
| The goal of this research has been to develop a formal and executable algebraic specification language which can be used to specify a variety of application programs, such as database systems, compilers and interpreters for programming languages, and business systems. An advantage of formality in this context is that each specification has a unique unambiguous meaning, so that it is actually meaningful to ask whether or not a given program ... |
|
Reports by Author
