{"entities":{"Q4229096":{"pageid":6258697,"ns":120,"title":"Item:Q4229096","lastrevid":108423077,"modified":"2026-11-06T09:51:13Z","type":"item","id":"Q4229096","labels":{},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1258216"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4229096$696FEF44-9484-45B1-8647-4D00394D6718","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0695195e4ca210b00bcb08bc3c13f9dc0b847583","datavalue":{"value":"0915.68006","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4229096$63C5D59A-D776-410B-830A-35CAABA6AA22","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"40f9dd054cdeb12941701947c800f4924d1843d2","datavalue":{"value":{"entity-type":"item","numeric-id":4229095,"id":"Q4229095"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4229096$19E951CA-B5F0-4591-93CF-4CA83FBC422A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f6bbd5c3b66d37fab966e520c3e67a514e12a0b3","datavalue":{"value":{"time":"+1999-03-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4229096$73553627-55DB-4AEA-9925-30185E349227","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ca8c16691e9ec83d46a3995338b09d48ac9660ac","datavalue":{"value":"68M10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4229096$256D7D81-27B9-48A1-AB4A-D1280CD1A895","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"24aafcf24a21bd70cd3b62d3f5f72a6d0d82d816","datavalue":{"value":"68-02","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4229096$49939DF1-0CD2-4F43-BADE-B86E4387EA31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a7dde57cbaf704d564d8f981ca98d6340e3d4aaf","datavalue":{"value":"68Q05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4229096$50B9F1DA-5C3B-40F3-8ACA-F7E4D91A3D0A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1025b6abca6fd250ca7102cb76c2bfb974c2b850","datavalue":{"value":"1258216","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4229096$BD88C0CE-F0CC-4C2A-B62E-E3C8165BF844","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b2d10fe87519b2960da5d3c9a27c66e8e2edb28c","datavalue":{"value":"design of distributed systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q4229096$3658B239-196C-4B93-854D-A24A80746667","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4229096$E1420529-36FF-445E-8E7C-77A07E88C1F9","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9da5b4ac30079ec985bc118bba22bf4a6cbb2161","datavalue":{"value":{"entity-type":"item","numeric-id":4702960,"id":"Q4702960"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"46f2e7520980f2cb5f3a8003a4058bf1fa6486f9","datavalue":{"value":{"amount":"+0.8089444041252136","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4229096$B99E3E44-FE0F-4A74-880D-A0625500BF37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1315c3d46788540da08311064cc764288e6d8bea","datavalue":{"value":{"entity-type":"item","numeric-id":6162110,"id":"Q6162110"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b98e5d158bba732b6fee807af2b5dddc72926d5e","datavalue":{"value":{"amount":"+0.7488467693328857","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4229096$7A999251-BEF0-4C17-8F1B-90BC6E03C2DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7de68a7eca1ccc5c178973b4db58983e3d9d1d13","datavalue":{"value":{"entity-type":"item","numeric-id":1177943,"id":"Q1177943"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b8d7eb23af607d93966a3462fb9f3597cd521d9d","datavalue":{"value":{"amount":"+0.7442607283592224","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4229096$CBF2F2B0-DC97-41BE-95BC-C9C1D3F48805","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3343eedbd4a09073ee0b27b6d8bef26f3ae938fa","datavalue":{"value":{"entity-type":"item","numeric-id":3510801,"id":"Q3510801"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e71eea513c0b1e8dce590fa3f6ff37f725f304ce","datavalue":{"value":{"amount":"+0.7432858943939209","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4229096$6ADEF76E-B687-4CB3-A67B-ADA15C26F86E","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"a854485daba0f90146047eced3790317e4e316bd","datavalue":{"value":"Diese Arbeit besch\u00e4ftigt sich mit dem formalen architekturbezogenen Entwurf verteilter Systeme. Ziel der Arbeit ist die Unterst\u00fctzung des hierarchischen Entwurfs durch eine Integration proze\u00dfalgebraischer und temporallogischer Spezifikations- und Verifikationstechniken. Die betrachteten Systeme bestehen aus einer gegebenen Anzahl von sequentiell arbeitenden Komponenten, die \u00fcber gemeinsame Aktionen kommunizieren. Durch die Verteilung der Systemaktionen auf die Komponenten ist die Kommunikationsstruktur und damit die Architektur festgelegt. Als Formalisierung eines Implementierungsschrittes im hierarchischen Entwurf wird die proze\u00dfalgebraische Methode der Aktionsverfeinerung betrachtet. Wir definieren eine lokalit\u00e4tsbasierte Proze\u00dfalgebra zur Spezifikation derartiger Systeme und entwickeln eine operationelle Semantik, die auch als eine kausalit\u00e4tsbasierte Semantik verstanden werden kann. Durch Aktionsverfeinerung kann die Implementierung einer Aktivit\u00e4t, die auf einer abstrakten Spezifikationsebene als eine Aktion betrachtet wurde, durch einen komplexen verteilten Proze\u00df beschrieben werden. Die Vorgabe der Systemarchitektur erlaubt es, f\u00fcr jede Komponente eine eigene lokale Implementierung einer abstrakten Aktion, an der mehrere Komponenten teilnehmen, anzugeben. Auf der Ebene einzelner Komponenten betrachtet entspricht dieser neue Verfeinerungsbegriff dem Konzept des Prozeduraufrufs in sequentiellen Systemen. Dadurch ist zwar die Implementierbarkeit innerhalb der vorgegebenen Architektur garantiert, allerdings k\u00f6nnen im allgemeinen ohne Analyse der Einzelkomponenten kaum Aussagen \u00fcber das Verhalten des Gesamtsystems nach einem Verfeinerungsschritt gemacht werden. Wir untersuchen daher Bedingungen an die Implementierungen einzelner Aktionen, die auch auf der Ebene der Systeme die Verwendung kompositioneller Beweistechniken aus der Theorie der Proze\u00dfalgebren f\u00fcr diesen Aktionsverfeinerungsbegriff erm\u00f6glichen. Zus\u00e4tzlich zeigen wir, wie restriktivere, aus der Literatur bekannte Verfeinerungsbegriffe mit Hilfe kanonischer Verfeinerungen in unseren Ansatz integriert werden k\u00f6nnen. Des weiteren wird die Vererbung von temporallogischen Anforderungsspezifikationen unter Aktionsverfeinerung untersucht. Das Ziel ist es, die Verifikation von Verhaltenseigenschaften auf der Implementierungsebene zu vermeiden oder wenigstens zu erleichtern, indem eine entsprechende Eigenschaft bereits auf der abstrakten Spezifikationsebene nachgewiesen wird. Wir diskutieren die Anforderungen, die eine temporale Logik erf\u00fcllen mu\u00df, um mit dem architekturbezogenen Ansatz einerseits und Aktionsverfeinerung andererseits vertr\u00e4glich zu sein. Eine geeignete Logik ist \\(\\nu\\)TrPTL, eine lokalit\u00e4tsbasierte Linear-Time-Logik, deren einzige temporale Operatoren Next-Modalit\u00e4ten sind, die \u00fcber dem Aktionsalphabet und den Komponenten parametrisiert sind. Die Ausdrucksst\u00e4rke der Logik wird \u00fcber Fixpunktoperatoren erreicht. Wir definieren drei Transformationen auf Teillogiken von \\(\\nu\\)TrPTL. Sie \u00fcberf\u00fchren temporallogische Formeln von der abstrakten Beschreibungsebene in Formeln f\u00fcr die Implementierungsebene auf Grundlage der proze\u00dfalgebraischen Beschreibung der Verfeinerung von Aktionen. Wir zeigen, da\u00df unter geeigneten Einschr\u00e4nkungen der Verfeinerungsfunktion eine temporallogische Formel genau dann f\u00fcr ein System gilt, wenn die transformierte Formel auf der Implementierungsebene erf\u00fcllt ist. Die Proze\u00dfalgebra enth\u00e4lt einen speziellen Operator zur Spezifikation von rekursivem Verhalten, f\u00fcr das Terminierung gew\u00e4hrleistet ist. Dieser Operator erlaubt es, derartiges endlich rekursives Verhalten in den Verfeinerungen der Aktionen zuzulassen und trotzdem die Vererbung von Lebendigkeitseigenschaften unter Verfeinerung nachzuweisen. Wir zeigen die N\u00fctzlichkeit dieses Operators anhand eines Beispiels, in dem eine Synchronisationsaktion mit Hilfe eines fehlerhaften \u00dcbertragungsmediums implementiert wird, das eine beliebige endliche Zahl von Nachrichten verlieren kann.","type":"string"},"datatype":"string"},"type":"statement","id":"Q4229096$4CAA0D7A-ED45-4AFD-8C15-AC623B902E2A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4229096","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4229096"}}}}}