Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben

2010 | Buch

Process Algebra Kapitel lesen Erstes Kapitel lesen

A Process Algebraic Approach to Software Architecture Design

verfasst von: Alessandro Aldini, Marco Bernardo, Flavio Corradini

Verlag: Springer London

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

Inthe?eldofformalmethodsincomputerscience,concurrencytheoryisreceivinga constantlyincreasinginterest.Thisisespeciallytrueforprocessalgebra.Althoughit had been originally conceived as a means for reasoning about the semantics of c- current programs, process algebraic formalisms like CCS, CSP, ACP, ?-calculus, and their extensions (see, e.g., [154,119,112,22,155,181,30]) were soon used also for comprehendingfunctionaland nonfunctionalaspects of the behaviorof com- nicating concurrent systems. The scienti?c impact of process calculi and behavioral equivalences at the base of process algebra is witnessed not only by a very rich literature. It is in fact worth mentioningthe standardizationprocedurethat led to the developmentof the process algebraic language LOTOS [49], as well as the implementation of several modeling and analysis tools based on process algebra, like CWB [70] and CADP [93], some of which have been used in industrial case studies. Furthermore, process calculi and behavioral equivalencesare by now adopted in university-levelcourses to teach the foundations of concurrent programming as well as the model-driven design of concurrent, distributed, and mobile systems. Nevertheless, after 30 years since its introduction, process algebra is rarely adopted in the practice of software development. On the one hand, its technica- ties often obfuscate the way in which systems are modeled. As an example, if a process term comprises numerous occurrences of the parallel composition operator, it is hard to understand the communicationscheme among the varioussubterms. On the other hand, process algebra is perceived as being dif?cult to learn and use by practitioners, as it is not close enough to the way they think of software systems.

Inhaltsverzeichnis

Frontmatter

Process Calculi and Behavioral Equivalences

Frontmatter
Chapter 1. Process Algebra
Abstract
Process algebra is a formal tool for the specification and the verification of concurrent and distributed systems. It supports compositional modeling through a set of operators able to express concepts like sequential composition, alternative composition, and parallel composition of action-based descriptions. It also supports mathematical reasoning via a two-level semantics, which formalizes the behavior of a description by means of an abstract machine obtained from the application of structural operational rules and then introduces behavioral equivalences able to relate descriptions that are syntactically different. In this chapter, we present the typical behavioral operators and operational semantic rules for a process calculus in which no notion of time, probability, or priority is associated with actions. Then, we discuss the three most studied approaches to the definition of behavioral equivalences – bisimulation, testing, and trace – and we illustrate their congruence properties, sound and complete axiomatizations, modal logic characterizations, and verification algorithms. Finally, we show how these behavioral equivalences and some of their variants are related to each other on the basis of their discriminating power.
Alessandro Aldini, Flavio Corradini, Marco Bernardo
Chapter 2. Deterministically Timed Process Algebra
Abstract
Concurrent and distributed systems are characterized not only by their functional behavior, but also by their quantitative features. A prominent role is played by timing aspects, which express the temporal execution of system activities. There are several different options for introducing time and time passing in system descriptions: durationless actions or durational actions, relative time or absolute time, global clock or local clocks. In this chapter, we present two timed process calculi arising from certain combinations of the options mentioned above, which share a deterministic representation of time and time passing suitable for real-time systems. Then, we show the impact of eager, lazy, and maximal progress interpretations of action execution on the expressiveness of timed descriptions and their bisimulation semantics. This is accomplished through a number of semantics-preserving mappings, which demonstrate how some of the different choices are not irreconcilable by providing a better understanding of benefits and drawbacks of the various time-related options.
Alessandro Aldini, Flavio Corradini, Marco Bernardo
Chapter 3. Stochastically Timed Process Algebra
Abstract
Timing aspects of concurrent and distributed systems can be expressed not only deterministically, but also probabilistically, which is particularly appropriate for shared-resource systems. When these aspects are modeled by using only exponentially distributed random variables, the stochastic process governing the system evolution over time turns out to be a Markov chain. From a process algebraic perspective, this limitation results in a simpler mathematical treatment both on the semantic side and on the stochastic side without sacrificing expressiveness. In this chapter, we introduce a Markovian process calculus with durational actions, then we discuss congruence properties, sound and complete axiomatizations, modal logic characterizations, and verification algorithms for Markovian versions of bisimulation equivalence, testing equivalence, and trace equivalence. We also examine a further property called exactness, which is related to Markov-chain-level aggregations induced by Markovian behavioral equivalences. Finally, we show how the linear-time/branching-time spectrum collapses in the Markovian case.
Alessandro Aldini, Flavio Corradini, Marco Bernardo

Process Algebra for Software Architecture

Frontmatter
Chapter 4. Component-Oriented Modeling
Abstract
Using process algebra at the software architecture level of design can be beneficial both for enhancing the usability of the formalism and for improving the formality and analyzability of the architectural descriptions. In fact, on the one hand process algebra is forced to support a friendly component-oriented way of modeling systems, while on the other hand the software designer can take advantage of a notation possessing a precise syntax and semantics as well as automated analysis techniques. In this chapter, we provide a number of guidelines for a principled transformation of process algebra into a fully fledged architectural description language called PADL. The guidelines, which favor specification reuse and insist on the elicitation of interfaces and communication features, are exemplified through the modeling of a client–server system and of a pipe–filter system.
Alessandro Aldini, Flavio Corradini, Marco Bernardo
Chapter 5. Component-Oriented Functional Verification
Abstract
Enhancing the usability of process algebra on the modeling side must be accompanied by an analogous effort on the verification side. At the architectural design level, it is important to detect mismatches stemming from the inappropriate assembly of several software units, which are correct when considered in isolation. In this chapter, we present a topological reduction process based on behavioral equivalences called MismDet, which exploits their congruence properties for efficiency reasons and their modal logic characterizations for diagnostic purposes. It investigates the absence of architectural mismatches in a component-oriented fashion by examining star-shaped and cycle-shaped topological portions. The application of the two techniques corresponding to the two topological formats, called architectural compatibility check and architectural interoperability check, is exemplified through the verification of a compressing proxy system and of a cruise control system.
Alessandro Aldini, Flavio Corradini, Marco Bernardo
Chapter 6. Component-Oriented Performance Evaluation
Abstract
The functional verification of software systems should not be separate from system performance evaluation. Any software architecture should be designed by having in mind the satisfaction of functional and nonfunctional requirements, and efforts should be made in order to understand whether the performance of a specific design can be improved. In addition to that, performance criteria should guide the choice among several alternative designs each of which is functionally correct. In this chapter, we present a procedure for the prediction, improvement, and comparison of the performance of architectural designs called PerfSel. It relies on the combined use of process algebraic architectural descriptions and queueing network models for assessing typical performance indices both at the system level and at the component level. Its application is exemplified through the performance comparison of three different architectures for a compiler system.
Alessandro Aldini, Flavio Corradini, Marco Bernardo
Chapter 7. Trading Dependability and Performance
Abstract
Modern software systems are often subject to dependability and performance requirements in conflict with each other. Since it is common to carry out separately dependability analysis and performance evaluation, the study of a tradeoff becomes hard to accomplish. In this chapter, we present DepPerf, a component-oriented methodology that can be used at the architectural design level for predicting the qualitative and quantitative impact of individual components on system dependability and performance. The methodology encompasses the behavioral equivalence approach to noninterference analysis and standard performance evaluation techniques, in order to reveal functional and nonfunctional dependences among components and then pinpoint the metrics to investigate for achieving a balanced tradeoff. The methodology is illustrated through its application to a secure routing system and to a power-manageable system.
Alessandro Aldini, Flavio Corradini, Marco Bernardo
Backmatter
Metadaten
Titel
A Process Algebraic Approach to Software Architecture Design
verfasst von
Alessandro Aldini
Marco Bernardo
Flavio Corradini
Copyright-Jahr
2010
Verlag
Springer London
Electronic ISBN
978-1-84800-223-4
Print ISBN
978-1-84800-222-7
DOI
https://doi.org/10.1007/978-1-84800-223-4

Premium Partner

    Bildnachweise