A Hierarchy of System Descriptions via Atomic Linear Refinement

The problem of relating system descriptions at different levels of abstraction is studied in the field of Process Description Languages, following the so-called interleaving approach. Since we believe that several different languages should be used profitably during the hierarchical specification process, we investigate the problem of implementing a calculus into another one. As a case study, we introduce a pair of languages which will be increasingly enriched. The basic languages are sequential and nondeterministic; their first enrichment is obtained by adding an operator for asynchrony; then also communication is added, and finally restriction is dealt with. For each pair, the latter language extends the former with atomicity, obtained by adding to the signature of the former an operator of strong prefixing that makes atomic the execution of a sequence of actions. The two languages are intended to be a specification and an implementation language, respectively. To directly relate them, a mapping, called atomic linear refinement, is introduced from actions of the former to atomic sequences (i.e. sequences of actions built with strong prefixing) of the latter. An atomic linear refinement can be homomorphically extended to become a mapping among process terms of the two languages and thus also among the states of their associated transition systems. A notion of implementation, based on a sort of bisimulation (parametric with respect to an atomic action refinement), relates processes of the two languages. Given a specification process p and an atomic action refinement ρ, the refined process ρ(p) is proved to be an implementation of p. Moreover, a complete proof system for strong and weak equivalence are presented for both languages (and thus also for the operator of strong prefixing) and proved consistent with respect to refinement: if p and ρ are congruent processes of the specification language, then ρ(p) and ρ(q) are congruent, too.

Download Full-text

TOWARDS HIERARCHICAL DESCRIPTION OF SYSTEMS: A PROOF SYSTEM FOR STRONG PREFIXING

International Journal of Foundations of Computer Science ◽

10.1142/s0129054190000205 ◽

1990 ◽

Vol 01 (03) ◽

pp. 277-293 ◽

Cited By ~ 7

Author(s):

ROBERTO GORRIERI ◽

UGO MONTANARI

Keyword(s):

Proof System ◽

Simple Extension ◽

Levels Of Abstraction ◽

Complete Proof ◽

Proof Systems ◽

Action Refinement ◽

Atomic Action ◽

Description Languages ◽

Different Levels

The problem of relating system descriptions at different levels of abstraction is addressed in the context of process description languages. As a case study, we introduce two nondeterministic languages. The latter is a simple extension of the former and is obtained by adding to its signature an operator of strong prefixing for making atomic the execution of a sequence of actions. The two languages are intended to be a specification and an implementation language, respectively. To directly relate them, we introduce a mapping, called atomic action refinement, from actions of the former to atomic sequences (i.e. sequences of actions built with strong prefixing) of the latter, which can be homomorphically extended to become a mapping among process terms of the two languages. A notion of implementation, based on a sort of bisimulation (parametric with respect to an atomic action refinement), relates processes of the two languages. Given a specification process P and an atomic action refinement ρ, the refined process ρ(P) is proved to be an implementation of P. Moreover, two complete proof systems for the two languages (and thus also for the operator of strong prefixing) are presented and proved consistent with respect to refinement: if P and Q are congruent processes of the specification language, then ρ(P) and ρ(Q) are congruent, too.

Download Full-text

Cryptographic Protocol Verification via Supercompilation (A Case Study)

10.29007/gpsh ◽

2018 ◽

Cited By ~ 1

Author(s):

Abdulbasit Ahmed ◽

Alexei Lisitsa ◽

Andrei Nemytykh

Keyword(s):

Program Transformation ◽

Cache Coherence ◽

Protocol Verification ◽

Cryptographic Protocol ◽

Levels Of Abstraction ◽

Transformation Techniques ◽

Program Specialization ◽

Coherence Protocols ◽

Different Levels

It has been known for a while that program transformation techniques, in particular, program specialization, can be used to prove the properties of programs automatically. For example, if a program actually implements (in a given context of use) a constant function, sufficiently powerful and semantics preserving program transformation may reduce the program to a syntactically trivial ``constant'' program, pruning unreachable branches and proving thereby the property. Viability of such an approach to verification has been demonstrated in previous works where it was applied to the verification of parameterized cache coherence protocols and Petri Nets models.In this paper we further extend the method and present a case study on its appication to the verification of a cryptographic protocol. The protocol is modeled by functional programs at different levels of abstraction and verification via program specialization is done by using Turchin's supercompilation method.

Download Full-text

Do semantic modal maps have a role in a constructionalization approach to modals?

Constructions and Frames ◽

10.1075/cf.8.1.07tra ◽

2016 ◽

Vol 8 (1) ◽

pp. 97-124 ◽

Cited By ~ 6

Author(s):

Elizabeth Closs Traugott

Keyword(s):

Construction Grammar ◽

Levels Of Abstraction ◽

Semantic Maps ◽

Micro Level ◽

Different Levels ◽

Over Time ◽

Conceptual Schemas

My aim in this paper is to show that, in modified form, semantic connectivity maps of the kind developed in van der Auwera & Plungian (1998) and van der Auwera (2013) can be useful for showing the development over time of relationships among polysemous constructions. Since these maps pertain primarily to meaning and are intended as contributions to cross-linguistic generalizations rather than to language-specific grammars, their purpose might seem orthogonal to construction grammar, in which form–meaning pairs are the basic units of grammar. I propose that the semantic maps can usefully be rethought as being of two kinds: schema-construction maps that represent relationships between abstract, conceptual schemas linked to underspecified form, and micro-construction maps that represent relationships between specific constructions. These two kinds of maps capture both form and meaning since they represent form–meaning pairings, but at different levels of abstraction. They can also capture direction of changes, as tendencies at the schema level and specific trajectories at the micro-level. My case study is the development of the marginal modals better, rather, sooner (see Denison & Cort 2010, van der Auwera & De Wit 2010). I show that better is significantly different in distribution and meaning from rather and sooner, and that, although they form a family of micro-constructions, they do not form a tight-knit group. This can be captured well by modified semantic maps.

Download Full-text

An Incidence Matrix Support for Conceptual Design Based on Port Ontology

Key Engineering Materials ◽

10.4028/www.scientific.net/kem.419-420.49 ◽

2009 ◽

Vol 419-420 ◽

pp. 49-52 ◽

Cited By ~ 1

Author(s):

Dong Xing Cao ◽

Zhan Wei Li ◽

Hong Lai Li ◽

Kai Cheng Qi

Keyword(s):

Conceptual Design ◽

Incidence Matrix ◽

Product Information ◽

Design Stage ◽

Design Decision ◽

Physical Domain ◽

Levels Of Abstraction ◽

Conceptual Design Stage ◽

Different Levels

Existing conceptual design methods mainly focus on component modeling and representation, which makes them insufficient to help in the conceptual design stage. Port ontology, as an approach to formally expressing product design, has been effectively applied to concept description of a product. An incidence matrix support for product conceptual design based on port ontology is given in this paper. It formally represents and organizes product information in both functional ontology and physical domain in a hierarchy. Port compatibilities are used to map and link the two components. This makes it possible to build incidence matrix and decompose it into an independence matrix, and allow designers from different backgrounds with various interests to access the design ontology. A multilevel matrix is constructed to generate principle schemes of products at different levels of abstraction, which facilitates design decision-making through the whole conceptual design stage. A case study is also given to demonstrate the proposed approach.

Download Full-text

A comparative study of modelling at different levels of abstraction in system on chip designs: a case study

IEEE Computer Society Annual Symposium on VLSI ◽

10.1109/isvlsi.2004.1339508 ◽

2004 ◽

Cited By ~ 7

Author(s):

S. Jayadevappa ◽

R. Shankar ◽

I. Mahgoub

Keyword(s):

Comparative Study ◽

System On Chip ◽

Levels Of Abstraction ◽

On Chip ◽

Different Levels

Download Full-text

Re-Interpretation of Conceptual Design Sketches in Mechanical Engineering

Volume 4: 13th International Conference on Design Theory and Methodology ◽

10.1115/detc2001/dtm-21711 ◽

2001 ◽

Author(s):

Martin Pache ◽

Anne Roemer ◽

Udo Lindemann ◽

Winfried Hacker

Keyword(s):

Engineering Design ◽

Conceptual Design ◽

Design Process ◽

Mechanical Engineering ◽

The Other ◽

Levels Of Abstraction ◽

Functional Elements ◽

Functional Features ◽

Different Levels

Abstract In this paper a case study on conceptual design in mechanical engineering design is presented. At first, an exemplary sketch from the design process is discussed with regard to the modality and level of abstraction of the elements used in this sketch. The possibility to predefine geometry of components, as well as functional features on different levels of abstraction provides clues for reinterpretation of the sketch. Furthermore a remarkable sequence of sketching is presented, that shows how reinterpretation of a sketch can result in significant changes of the conceptual solution. This may be due to the combination of geometrical and functional elements, that gain meaning within the overall context of the sketch only in combination with the other elements. Therefore recombination by reinterpretation may change this context entirely. The proposed mechanisms could not be verified due to the rareness of their occurrence, still these mechanisms may have a significant impact on a design process. Therefore this paper is supposed to provide hypotheses for further research on this subject.

Download Full-text

Digital Twin for Designing and Reconfiguring Human–Robot Collaborative Assembly Lines

Applied Sciences ◽

10.3390/app11104620 ◽

2021 ◽

Vol 11 (10) ◽

pp. 4620

Author(s):

Niki Kousi ◽

Christos Gkournelos ◽

Sotiris Aivaliotis ◽

Konstantinos Lotsaris ◽

Angelos Christos Bavelos ◽

...

Keyword(s):

Production System ◽

Assembly Lines ◽

Flexible Assembly ◽

Digital Twin ◽

Collaborative Assembly ◽

Geometrical Information ◽

Line Level ◽

Dual Arm ◽

Different Levels

This paper discusses a digital twin-based approach for designing and redesigning flexible assembly systems. The digital twin allows modeling the parameters of the production system at different levels including assembly process, production station, and line level. The approach allows dynamically updating the digital twin in runtime, synthesizing data from multiple 2D–3D sensors in order to have up-to-date information about the actual production process. The model integrates both geometrical information and semantics. The model is used in combination with an artificial intelligence logic in order to derive alternative configurations of the production system. The overall approach is discussed with the help of a case study coming from the automotive industry. The case study introduces a production system integrating humans and autonomous mobile dual arm workers.

Download Full-text