Specification and verification using a visual formalism on top of temporal logic

1996 ◽  
pp. 305-339
Author(s):  
Hardi Hungar
Keyword(s):  
Temporal Logic ◽  
Specification And Verification

Specification and Verification of the ATMR Protocol Using UNITY: Part 1: Modeling and Specification of the Protocal

1998 ◽  
Vol 08 (04) ◽  
pp. 421-432 ◽  
Author(s):  
Michel Charpentier ◽  
Gérard Padiou
Keyword(s):  
Quality Assurance ◽  
Temporal Logic ◽  
Development Process ◽  
Detection Algorithm ◽  
Formal Description ◽  
General Development ◽  
Correctness Proof ◽  
Program Specification ◽  
Specification And Verification

We propose a description and validation of the ATMR protocol within the UNITY formalism. This formal description helps us understand precisely the mechanisms this protocol involves. In particular, we have noted the use of an incorrect detection algorithm to generate reset slots. In this first part, we provide an operational description using the UNITY programming notation as well as a specification of the main correctness properties in the UNITY temporal logic. A second part [2] is dedicated to a hand-made correctness proof. The proof shows that the model satisfies the specification despite this spurious detection. In this study, we apply a general development process based upon the UNITY formalism. During this process, we tune the program specification in order to make the later validation step easier, in the same way as the inclusion of traces, breakpoints, and assertions prepares a program for its quality assurance tests.

SPECIFICATION AND VERIFICATION OF COMMUNICATION CONSTRAINTS FOR INTEROPERABLE TRANSACTIONS

1994 ◽  
Vol 03 (01) ◽  
pp. 47-65 ◽  
Author(s):  
A HH NGU ◽  
R MEERSMAN ◽  
H WEIGAND
Keyword(s):  
Temporal Logic ◽  
Dependency Graph ◽  
Communication Behavior ◽  
Communication Constraints ◽  
Transaction Model ◽  
Tableau Method ◽  
Component Systems ◽  
Specification And Verification ◽  
Business Trip ◽  
Temporal Ordering

The specification of communication behavior is fundamental in developing interoperable transactions. In particular, the temporal ordering of messages exchanged between different communicating agents must be declaratively specified and verified in order to guarantee consistency of data in the various component systems. This paper shows that by expressing communication constraints in propositional temporal logic, the tableau method can be applied to construct a dependency graph. If the specification is correct, this method guarantees that all possible execution paths satisfying the specification will be generated. The declarative specification and verification of communication constraints in interoperable transactions is demonstrated using the classic business trip. It is argued that the specification formalism provides an improvement over the Flexible Transaction Model.

scholarly journals Specification and verification of an attribute-based usage control approach for open and dynamic computing environments

2014 ◽  
Author(s):  
Χρήστος Γρομπανόπουλος
Keyword(s):  
Internet Of Things ◽  
Ubiquitous Computing ◽  
Temporal Logic ◽  
Usage Control ◽  
Control Approach ◽  
Computing Environments ◽  
Specification And Verification ◽  
Temporal Logic Of Actions

Τα υπολογιστικά συστήματα εξελίσσονται συνεχώς προκειμένου να αντεπεξέλθουν στις απαιτήσεις που θέτουν οι χρήστες τους. Η εξάπλωση των τεχνολογιών δικτύου οδήγησε στη μετάβαση από το μοντέλο αυτόνομου υπολογιστή στο μοντέλο εξυπηρετητή – πελάτη. Επιπρόσθετα, κοινωνικές τάσεις όπως η συχνή μετακίνηση και η κοινωνική δικτύωση οδήγησαν στη δημιουργία υπολογιστικών συσκευών μικρών σε μέγεθος, οι οποίες είναι εξοπλισμένες με αισθητήρες προκειμένου να αναγνωρίζουν το περιβάλλον και να προσαρμόζουν αντίστοιχα τη λειτουργία τους σε αυτό. Κατά συνέπεια, προέκυψαν καινούργια υπολογιστικά περιβάλλοντα όπως το περιβάλλον διάχυτης υπολογιστικής (ubiquitous computing), τα περιβάλλοντα πλαισίου (grid) – σύννεφου (cloud) και το διαδίκτυο των πραγμάτων (Internet of Things). Τα προαναφερόμενα υπολογιστικά περιβάλλοντα δημιουργούν νέες απαιτήσεις σε διάφορους τομείς, συμπεριλαμβανομένου και αυτού της ασφάλειας, της οποίας ο ρόλος είναι εξέχουσας σημασίας. Συγκεκριμένα, όσον αφορά την ασφάλεια υπολογιστών και ειδικότερα τον έλεγχο πρόσβασης, η εξέλιξη των υπολογιστικών συστημάτων συνετέλεσε στη δημιουργία των Ανοιχτών και Δυναμικών Υπολογιστικών Περιβαλλόντων (ΑΔΥΠ). Τα ΑΔΥΠ χαρακτηρίζονται ως ανοιχτά μιας και δεν υπάρχει σαφές όριο ανάμεσα στους εξουσιοδοτημένους και τους παράνομους χρήστες του συστήματος. Επίσης χαρακτηρίζονται ως δυναμικά καθώς η σύνθεσή τους συνεχώς μεταβάλλεται. Επιπρόσθετα, οι υπάρχουσες προσεγγίσεις ελέγχου πρόσβασης δεν έχουν σχεδιαστεί για την εφαρμογής τους στα ΑΔΥΠ, γεγονός που μας οδηγεί στο συμπέρασμα ότι δεν μπορούν να ικανοποιήσουν πλήρως τις μοναδικές απαιτήσεις που τα ίδια θέτουν. Κατά συνέπεια, απαιτείται μια ενδελεχής ανάλυση των απαιτήσεων αναφορικά με τα μοντέλα ελέγχου πρόσβασης που στοχεύουν στα ΑΔΥΠ, η οποία επακόλουθα θα βοηθήσει στον ορισμό κατάλληλων προσεγγίσεων ελέγχου πρόσβασης για την εφαρμογή τους σε αυτά.Σε αυτή τη διατριβή αναλύουμε τις υπάρχουσες προτάσεις ελέγχου πρόσβασης και χρήσης, με σκοπό να αναγνωρίσουμε έναν αριθμό μοναδικών απαιτήσεων που θέτουν τα ΑΔΥΠ. Κατά δεύτερο λόγο, ορίζουμε φορμαλιστικά ένα μοντέλο ελέγχου χρήσης βασιζόμενοι σε χαρακτηριστικά για τα ΑΔΥΠ, το οποίο σχεδιάστηκε βάσει των απαιτήσεων που εντοπίστηκαν. Τελευταίο μα όχι λιγότερο σημαντικό, ελέγχουμε το προτεινόμενο μοντέλο για την ορθότητά του, δηλαδή την προσήλωσή του στις αρχικά οριζόμενες απαιτήσεις.Συγκεκριμένα, παρουσιάζουμε πληροφορίες για τα RBAC, ABAC, και UCON μοντέλα, τα οποία κατά κόρον εφαρμόζονται στην εξεταζόμενη περίπτωση των ΑΔΥΠ. Επίσης, αναφέρουμε πληροφορίες σχετικές με τη μοντελοποίηση παράλληλων συστημάτων, όπως τα συστήματα ελέγχου πρόσβασης. Οι προαναφερόμενες πληροφορίες συνεισφέρουν στην αναγνώριση των προδιαγραφών στο πλαίσιο της μοντελοποίησης των μοντέλων ελέγχου πρόσβασης/χρήσης στα ΑΔΥΠ. Επιπρόσθετα, περιγράφουμε σύγχρονες τεχνικές επαλήθευσης, καθώς απαιτείται ο έλεγχος της ορθότητας των εκ νέου οριζόμενων μοντέλων σε σχέση με τις αρχικά οριζόμενες προδιαγραφές τους. Στη συνέχεια, τονίζουμε μέσω αντιπροσωπευτικών σεναρίων χρήσεων τις προκλήσεις και τους περιορισμούς που ενυπάρχουν κατά την προσπάθεια αξιοποίησης της οικογένειας μοντέλων UCON στα σύγχρονα υπολογιστικά περιβάλλοντα.Με σκοπό να ικανοποιήσουμε τις απαιτήσεις που θέτουν τα ΑΔΥΠ προτείνουμε και ορίζουμε μια αυστηρά φορμαλιστική περιγραφή του μοντέλου UseCON χρησιμοποιώντας την Temporal Logic of Actions (TLA+) γλώσσα φορμαλισμού. Στη συνέχεια πραγματοποιούμε μια αποτίμηση του UseCON, το οποίο εμπεριέχει έναν αριθμό σημαντικών χαρακτηριστικών συγκρινόμενο με τα υπάρχοντα μοντέλα ελέγχου πρόσβασης/χρήσης. Καταρχάς, το προτεινόμενο μοντέλο παρουσιάζει επαυξημένη εκφραστικότητα συγκρινόμενο με τα υπάρχοντα μοντέλα ελέγχου χρήσης, εξαιτίας της ικανότητάς του να αξιοποιεί πληροφορία προερχόμενη είτε από μία είτε από ένα σύνολο από άμεσες και έμμεσες οντότητες κατά τη διάρκεια της δημιουργίας απόφασης για επιτρεπόμενη πρόσβαση. Κατά δεύτερο λόγο, το UseCON εγγενώς υποστηρίζει την αξιοποίηση της πληροφορίας που αφορά ιστορικό χρήσεων διαμέσου της αυτοματοποιημένης διαχείρισης των χρήσεων. Επιπρόσθετα πλεονεκτήματα του προτεινόμενου μοντέλου είναι η δυνατότητα υποστήριξης απλοποιημένης διαδικασίας διαχείρισης πολιτικών και η υποστήριξη επαυξημένων κανόνων πολιτικών όσον αφορά την εκφραστικότητά τους.Με στόχο την απόδειξη της ορθότητας του μοντέλου UseCON που ορίσαμε πραγματοποιούμε έρευνα σχετική με τεχνικές φορμαλιστικής επαλήθευσης, που έχει ως αποτέλεσμα τον ορισμό ενός συνόλου ιδιοτήτων ασφάλειας και ζωτικότητας. Η επαλήθευση αυτού του συνόλου ιδιοτήτων πραγματοποιήθηκε με την εφαρμογή μιας τεχνικής ελέγχου μοντέλων που χρησιμοποιεί τον TLC. Τέλος, ολοκληρώνουμε αυτή τη διατριβή με την παράθεση επιπρόσθετων πληροφοριών αναφορικά με τη διαδικασία επαλήθευσης με τη χρήση του TLC και αναλύουμε περαιτέρω τα ευρήματά μας καθορίζοντας τις συνεισφορές αυτής της ερευνητικής εργασίας καθώς και τις πιθανές μελλοντικές κατευθύνσεις έρευνας.

Specification and Verification of the ATMR Protocol Using UNITY: Part 2: Correctness Proof

1998 ◽  
Vol 08 (04) ◽  
pp. 433-445 ◽  
Author(s):  
Michel Charpentier ◽  
Gérard Padiou
Keyword(s):  
Temporal Logic ◽  
Detection Algorithm ◽  
Generation Mechanism ◽  
Formal Description ◽  
Correctness Proof ◽  
Previous Part ◽  
Specification And Verification

We propose a description and validation of the ATMR protocol within the UNITY formalism. This formal description helps us understand precisely the mechanisms this protocol involves. In particular, we have noted the use of an incorrect detection algorithm to generate reset slots. An operational description using the UNITY programming notation and a specification of the main correctness properties in the UNITY temporal logic are given in a previous part [2]. This second part is dedicated to a hand-made correctness proof. The proof shows that the model satisfies the specification despite the spurious detection in the reset generation mechanism.

scholarly journals Tableau-Like Automata-Based Axiomatization for Propositional Linear Temporal Logic

10.29007/df56 ◽  
2018 ◽  
Author(s):  
Nikolay V. Shilov
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Decision Procedure ◽  
Computer Programs ◽  
Linear Temporal Logic ◽  
Local Model ◽  
Specification And Verification ◽  
Local Model Checking

Propositional Linear Temporal Logic (PLTL) is a very popular formalism for specification and verification of computer programs and systems. This extended abstract sketches a tableau-like axiomatization for PLTL based on automata-theoretic decision procedure coupled with tableau for local model checking of the propositional μ-Calculus.

Sign in / Sign up

Export Citation Format

Share Document