Compositional refinements in multiple blackboard systems
Identifieur interne : 00D032 ( Main/Merge ); précédent : 00D031; suivant : 00D033Compositional refinements in multiple blackboard systems
Auteurs : X. J. Chen [Italie] ; C. Montangero [Italie]Source :
- Acta Informatica [ 0001-5903 ] ; 1995-05-01.
English descriptors
- Teeft :
- Aact, Acomp, Active component, Active components, Agent action, Agent information, Agent state, Agent transition, Agent transitions, Ainfor, Algebraic, Astate, Axiom, Blackboard, Blackboard comb, Blackboard exploits unification, Blackboard names, Blackboard paradigm, Blackboard system, Blackboard systems, Blackboard tree, Body part, Chen, Compositional, Compositional refinements, Concurrent system, Concurrent system conesp, Concurrent systems, Cond, Conesp, Coord, Direct proof, Direct proofs, Dynamic algebra, Dynamic specification, Endspec, Endspec table, Equivalent definition, Facts unifiable, Failure out_set, Final condition, First case, First pattern, Formal specification, General ones, General state, General states, Global, Global information, High priority consumer, Implementation relationship, Infor, Initial state, Input action, Input facts, Internal action, Intuitive meaning, Knowledge base, Lncs, Logic programming, Monitoring step, Montangero, Mset, Multiple blackboard systems, Multiset, Next state, Oikos, Other words, Out_set, Pages lncs, Parallelism, Parallelism step, Partial moves, Passive component, Passive components, Pattern activation, Pcomb, Predicate, Prog, Prolog, Prolog execution, Prolog goal, Prolog program, Refinement, Root name, Sact, Sect, Semantics, Seqlmp, Seqspec, Sequential, Sequential machine, Smolcs, Smolcs methodology, Software, Software process modelling, Software process models, Spec, Specification, Subset, Substitution, Subsystem, Super system, Synchronization, Synchronization step, System axioms, System termination, System transition, System transitions, Theory coord, Theory pcomb, Transition predicate, Transition relationship, Transition system, Transition systems.
Abstract
Abstract: In this paper we introduce CONESP, a concurrent system built according to the SMoLCS methodology to provide an abstract model of the coordination language Extended Shared Prolog (ESP), which is based on the integration of the blackboard paradigm with Logic Programming. CONESP is a hierarchy of blackboard systems, each consisting of a passive blackboard tree and a collection of active components including parallel agents and dynamic (sub)systems. An implementation relationshop between two hierarchies is defined, which is shown to be compositional. Some techniques have also been developed for the direct proof, i.e. the basic step in the inductive proof that one system implements another. ESP is being used in the Oikos environment for software process modelling. The results of this paper are the basis for the formal verification of the correctness of the software process models built by stepwise-refinements in Oikos.
Url:
DOI: 10.1007/BF01213078
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 003326
- to stream Istex, to step Curation: 003284
- to stream Istex, to step Checkpoint: 002B90
Links to Exploration step
ISTEX:D6F5BE2E912603B0B6979C213D19338B5C24C008Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Compositional refinements in multiple blackboard systems</title><author><name sortKey="Chen, X J" sort="Chen, X J" uniqKey="Chen X" first="X. J." last="Chen">X. J. Chen</name></author><author><name sortKey="Montangero, C" sort="Montangero, C" uniqKey="Montangero C" first="C." last="Montangero">C. Montangero</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:D6F5BE2E912603B0B6979C213D19338B5C24C008</idno><date when="1995" year="1995">1995</date><idno type="doi">10.1007/BF01213078</idno><idno type="url">https://api.istex.fr/ark:/67375/1BB-V90C8VZZ-P/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003326</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003326</idno><idno type="wicri:Area/Istex/Curation">003284</idno><idno type="wicri:Area/Istex/Checkpoint">002B90</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002B90</idno><idno type="wicri:doubleKey">0001-5903:1995:Chen X:compositional:refinements:in</idno><idno type="wicri:Area/Main/Merge">00D032</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Compositional refinements in multiple blackboard systems</title><author><name sortKey="Chen, X J" sort="Chen, X J" uniqKey="Chen X" first="X. J." last="Chen">X. J. Chen</name><affiliation wicri:level="3"><country xml:lang="fr">Italie</country><wicri:regionArea>Scuola Normale Superiore, Piazza dei Cavalieri 7, I-56100, Pisa</wicri:regionArea><placeName><settlement type="city">Pise</settlement><region nuts="2">Toscane</region></placeName></affiliation></author><author><name sortKey="Montangero, C" sort="Montangero, C" uniqKey="Montangero C" first="C." last="Montangero">C. Montangero</name><affiliation wicri:level="4"><country xml:lang="fr">Italie</country><wicri:regionArea>Dipartimento di Informatica, Università di Pisa, Corso Italia 40, I-56100, Pisa</wicri:regionArea><placeName><settlement type="city">Pise</settlement><region nuts="2">Toscane</region></placeName><orgName type="university">Université de Pise</orgName></affiliation></author></analytic><monogr></monogr><series><title level="j">Acta Informatica</title><title level="j" type="abbrev">Acta Informatica</title><idno type="ISSN">0001-5903</idno><idno type="eISSN">1432-0525</idno><imprint><publisher>Springer-Verlag</publisher><pubPlace>Berlin/Heidelberg</pubPlace><date type="published" when="1995-05-01">1995-05-01</date><biblScope unit="volume">32</biblScope><biblScope unit="issue">5</biblScope><biblScope unit="page" from="415">415</biblScope><biblScope unit="page" to="458">458</biblScope></imprint><idno type="ISSN">0001-5903</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0001-5903</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="Teeft" xml:lang="en"><term>Aact</term><term>Acomp</term><term>Active component</term><term>Active components</term><term>Agent action</term><term>Agent information</term><term>Agent state</term><term>Agent transition</term><term>Agent transitions</term><term>Ainfor</term><term>Algebraic</term><term>Astate</term><term>Axiom</term><term>Blackboard</term><term>Blackboard comb</term><term>Blackboard exploits unification</term><term>Blackboard names</term><term>Blackboard paradigm</term><term>Blackboard system</term><term>Blackboard systems</term><term>Blackboard tree</term><term>Body part</term><term>Chen</term><term>Compositional</term><term>Compositional refinements</term><term>Concurrent system</term><term>Concurrent system conesp</term><term>Concurrent systems</term><term>Cond</term><term>Conesp</term><term>Coord</term><term>Direct proof</term><term>Direct proofs</term><term>Dynamic algebra</term><term>Dynamic specification</term><term>Endspec</term><term>Endspec table</term><term>Equivalent definition</term><term>Facts unifiable</term><term>Failure out_set</term><term>Final condition</term><term>First case</term><term>First pattern</term><term>Formal specification</term><term>General ones</term><term>General state</term><term>General states</term><term>Global</term><term>Global information</term><term>High priority consumer</term><term>Implementation relationship</term><term>Infor</term><term>Initial state</term><term>Input action</term><term>Input facts</term><term>Internal action</term><term>Intuitive meaning</term><term>Knowledge base</term><term>Lncs</term><term>Logic programming</term><term>Monitoring step</term><term>Montangero</term><term>Mset</term><term>Multiple blackboard systems</term><term>Multiset</term><term>Next state</term><term>Oikos</term><term>Other words</term><term>Out_set</term><term>Pages lncs</term><term>Parallelism</term><term>Parallelism step</term><term>Partial moves</term><term>Passive component</term><term>Passive components</term><term>Pattern activation</term><term>Pcomb</term><term>Predicate</term><term>Prog</term><term>Prolog</term><term>Prolog execution</term><term>Prolog goal</term><term>Prolog program</term><term>Refinement</term><term>Root name</term><term>Sact</term><term>Sect</term><term>Semantics</term><term>Seqlmp</term><term>Seqspec</term><term>Sequential</term><term>Sequential machine</term><term>Smolcs</term><term>Smolcs methodology</term><term>Software</term><term>Software process modelling</term><term>Software process models</term><term>Spec</term><term>Specification</term><term>Subset</term><term>Substitution</term><term>Subsystem</term><term>Super system</term><term>Synchronization</term><term>Synchronization step</term><term>System axioms</term><term>System termination</term><term>System transition</term><term>System transitions</term><term>Theory coord</term><term>Theory pcomb</term><term>Transition predicate</term><term>Transition relationship</term><term>Transition system</term><term>Transition systems</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: In this paper we introduce CONESP, a concurrent system built according to the SMoLCS methodology to provide an abstract model of the coordination language Extended Shared Prolog (ESP), which is based on the integration of the blackboard paradigm with Logic Programming. CONESP is a hierarchy of blackboard systems, each consisting of a passive blackboard tree and a collection of active components including parallel agents and dynamic (sub)systems. An implementation relationshop between two hierarchies is defined, which is shown to be compositional. Some techniques have also been developed for the direct proof, i.e. the basic step in the inductive proof that one system implements another. ESP is being used in the Oikos environment for software process modelling. The results of this paper are the basis for the formal verification of the correctness of the software process models built by stepwise-refinements in Oikos.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00D032 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 00D032 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Merge
|type= RBID
|clé= ISTEX:D6F5BE2E912603B0B6979C213D19338B5C24C008
|texte= Compositional refinements in multiple blackboard systems
}}
| This area was generated with Dilib version V0.6.33. |  |