Λογισμός των Επικοινωνούντων Συστημάτων

Ο Λογισμός των Επικοινωνούντων Συστημάτων (Calculus of Communicating Systems ή CCS) είναι ένας λογισμός διεργασιών (process calculus) που εμφανίστηκε τη δεκαετία του 1980 από τον Robin Milner και ονομάστηκε από τον τίτλο του βιβλίου που περιέγραφε το λογισμό. Οι ενέργειές του μοντελοποιούν αδιαίρετες επικοινωνίες μεταξύ ακριβώς δύο συμμετεχόντων. Η τυπική γλώσσα περιλαμβάνει βασικά στοιχεία για την περιγραφή της παράλληλης σύνθεσης, της επιλογής μεταξύ ενεργειών και του περιορισμού εμβέλειας. Ο CCS είναι χρήσιμος για την εκτίμηση της ορθότητας ιδιοτήτων ενός συστήματος όπως τα αδιέξοδα (deadlocks) και τα ζωντανά αδιέξοδα (livelocks).^[1]

Σύμφωνα με το Milner, "Δεν υπάρχει κάτι κανονικό σχετικά με την επιλογή των βασικών συνδυαστών, αν και επιλέχθηκαν με προσοχή στην οικονομία. Αυτό που χαρακτηρίζει το λογισμό μας δεν είναι η ακριβής επιλογή των συνδυαστών αλλά η επιλογή της ερμηνείας και του μαθηματικού πλαισίου".^[2]

Οι εκφράσεις της γλώσσας ερμηνεύονται σαν συστήματα μεταβάσεων με ετικέτες (labelled transition systems). Ανάμεσα σε αυτά τα μοντέλα, σαν σημασιολογική ισοδυναμία χρησιμοποιείται η αμφιομοιότητα (bisimilarity).

Σύνταξη[Επεξεργασία | επεξεργασία κώδικα]

Δεδομένου ενός συνόλου από ονόματα ενεργειών, το σύνολο των διεργασιών του CCS ορίζεται από την εξής γραμματική BNF:

P::=\emptyset \,\,\,|\,\,\,a.P_{1}\,\,\,|\,\,\,A\,\,\,|\,\,\,P_{1}+P_{2}\,\,\,|\,\,\,P_{1}|P_{2}\,\,\,|\,\,\,P_{1}[b/a]\,\,\,|\,\,\,P_{1}{\backslash }a\,\,\,

Τα μέρη της σύνταξης, με τη σειρά που δόθηκαν παραπάνω, είναι

κενή διεργασία: η κενή διεργασία $\emptyset$ είναι έγκυρη διεργασία του CCS
ενέργεια: η διεργασία $a.P_{1}$ μπορεί να εκτελέσει μια ενέργεια $a$ και συνεχίζει σαν διεργασία $P_{1}$
αναγνωριστικό διεργασίας: γράφεται σαν $A{\overset {\underset {\mathrm {def} }{}}{=}}P_{1}$ για να χρησιμοποιήσει το αναγνωριστικό $A$ για να αναφερθεί στη διαδικασία $P_{1}$
επιλογή: η επιλογή $P_{1}+P_{2}$ μπορεί να προχωρήσει είτε σαν διαδικασία $P_{1}$ είτε σαν διαδικασία $P_{2}$
παράλληλη σύνθεση: η $P_{1}|P_{2}$ δηλώνει ότι οι διεργασίες $P_{1}$ και $P_{2}$ υπάρχουν την ίδια στιγμή
μετονομασία: η $P_{1}[b/a]$ είναι η διεργασία $P_{1}$ με όλες τις ενέργειες με όνομα $a$ να μετονομάζονται σαν $b$
περιορισμός: η $P_{1}{\backslash }a$ είναι η διεργασία $P_{1}$ χωρίς την ενέργεια $a$

Σχετικοί λογισμοί και μοντέλα[Επεξεργασία | επεξεργασία κώδικα]

Επικοινωνούσες Ακολουθιακές Διεργασίες (Communicating Sequential Processes, CSP), από τον Τόνυ Χόαρ, μια γλώσσα που εμφανίστηκε την ίδια εποχή με τον CCS.
Ο π-λογισμός (pi-calculus), που αναπτύχθηκε από το Milner στα τέλη της δεκαετίας του 1980, προσφέρει κινητικότητα (mobility) των επικοινωνιών, επιτρέποντας στις διεργασίες να ανταλλάσσουν ονόματα καναλιών επικοινωνίας.
Η PEPA, αναπτύχθηκε από τη Jane Hillston και εισάγει χρονισμό ενεργειών (activity timing) και πιθανοτική επιλογή (probabilistic choice), επιτρέποντας μετρήσεις αποδοτικότητας.

Κάποιες άλλες γλώσσες που βασίστηκαν στο CCS:

Μοντέλα που έχουν χρησιμοποιηθεί στη μελέτη συστημάτων τύπου CCS:

Παραπομπές[Επεξεργασία | επεξεργασία κώδικα]

↑ Herzog, Ulrich, επιμ. (2007). «Tackling Large State Spaces in Performance Modelling». Formal Methods for Performance Evaluation. Lecture Notes in Computer Science. 4486. Springer. σελίδες 318–370. doi:10.1007/978-3-540-72522-0. Αρχειοθετήθηκε από το πρωτότυπο στις 12 Απριλίου 2008. Ανακτήθηκε στις 21 Απριλίου 2009.
↑ "There is nothing canonical about the choice of the basic combinators, even though they were chosen with great attention to economy. What characterises our calculus is not the exact choice of combinators, but rather the choice of interpretation and of mathematical framework"

Αναφορές[Επεξεργασία | επεξεργασία κώδικα]

Robin Milner: A Calculus of Communicating Systems, Springer Verlag, ISBN 0-387-10235-3. 1980.
Robin Milner, Communication and Concurrency, Prentice Hall, International Series in Computer Science, ISBN 0-131-15007-3. 1989

[1] Herzog, Ulrich, επιμ. (2007). «Tackling Large State Spaces in Performance Modelling». Formal Methods for Performance Evaluation. Lecture Notes in Computer Science. 4486. Springer. σελίδες 318–370. doi:10.1007/978-3-540-72522-0. Αρχειοθετήθηκε από το πρωτότυπο στις 12 Απριλίου 2008. Ανακτήθηκε στις 21 Απριλίου 2009.

[2] "There is nothing canonical about the choice of the basic combinators, even though they were chosen with great attention to economy. What characterises our calculus is not the exact choice of combinators, but rather the choice of interpretation and of mathematical framework"

[1]

[2]