We're sorry but this page doesn't work properly without JavaScript enabled. Please enable it to continue.
Feedback

Formal methods: Monitoring Distributed Systems under Partial Synchrony

00:00

Formale Metadaten

Titel
Formal methods: Monitoring Distributed Systems under Partial Synchrony
Serientitel
Anzahl der Teile
30
Autor
Lizenz
CC-Namensnennung 4.0 International:
Sie dürfen das Werk bzw. den Inhalt zu jedem legalen Zweck nutzen, verändern und in unveränderter oder veränderter Form vervielfältigen, verbreiten und öffentlich zugänglich machen, sofern Sie den Namen des Autors/Rechteinhabers in der von ihm festgelegten Weise nennen.
Identifikatoren
Herausgeber
Erscheinungsjahr
Sprache

Inhaltliche Metadaten

Fachgebiet
Genre
Abstract
In this paper, we study the problem of runtime verification of distributed applications that do not share a global clock with respect to specifications in the linear temporal logics (LTL). Our proposed method distinguishes from the existing work in three novel ways. First, we make a practical assumption that the distributed system under scrutiny is augmented with a clock synchronization algorithm that guarantees bounded clock skew among all processes. Second, we do not make any assumption about the structure of predicates that form LTL formulas. This relaxation allows us to monitor a wide range of applications that was not possible before. Subsequently, we propose a distributed monitoring algorithm by employing SMT solving techniques. Third, given the fact that distributed applications nowadays run on massive cloud services, we extend our solution to a parallel monitoring algorithm to utilize the available computing infrastructure. We report on rigorous synthetic as well as real-world case studies and demonstrate that scalable online monitoring of distributed applications is within our reach.
AggregatzustandSynchronisierungPartielle DifferentiationLaufzeitfehlerProgrammverifikationSynchronisierungPartielle Differentiationt-TestData MiningRechter WinkelProgrammverifikationLaufzeitfehlerJSONXML
ProgrammverifikationLaufzeitfehlerPhysikalisches SystemUnendlichkeitEreignishorizontDifferenteOrdnung <Mathematik>AbstraktionsebeneAlgorithmusPrädikat <Logik>SystemprogrammierungStreaming <Kommunikationstechnik>Partielle DifferentiationSynchronisierungZeitsynchronisationSchiefe WahrscheinlichkeitsverteilungFontLineare AbbildungTemporale LogikKontextbezogenes SystemMaßerweiterungAusdruck <Logik>Funktion <Mathematik>Virtuelle MaschineEindeutigkeitDeterministischer ProzessTransaktionSoftwareProzess <Informatik>Relation <Informatik>Prozess <Informatik>AggregatzustandFigurierte ZahlEreignishorizontPhysikalisches SystemMultiplikationsoperatorOffice-PaketExplosion <Stochastik>InstantiierungStellenringGradientUmwandlungsenthalpieGruppenoperationKategorie <Mathematik>Web SiteVerschlingungOrdnung <Mathematik>Rechter WinkelSynchronisierungSoundverarbeitungAusdruck <Logik>Zentrische StreckungSchnittmengeGüte der AnpassungKontextbezogenes SystemPhysikalischer EffektWhiteboardGeradeProjektive EbeneGrenzwertberechnungMAPDeterminanteZellularer AutomatInverser LimesNeuroinformatikNummernsystemFlächeninhaltt-TestGibbs-VerteilungBildschirmfensterVererbungshierarchieTopologieFormale SemantikNichtlinearer OperatorEinsMathematikTelekommunikationEntscheidungstheorieFamilie <Mathematik>ZustandsmaschineAlgorithmusPrädikat <Logik>RoboterLaufzeitfehlerLeistungsbewertungProgrammverifikationGebundener ZustandAuflösung <Mathematik>Schiefe WahrscheinlichkeitsverteilungUnendlichkeitAblaufverfolgungTemporale LogikTermMechanismus-Design-TheoriePartielle DifferentiationComputersimulationParallelrechnerVarietät <Mathematik>Computeranimation
Prozess <Informatik>StellenringFunktion <Mathematik>Schiefe WahrscheinlichkeitsverteilungLokales MinimumEreignishorizontMessage-PassingDynamisches RAMTeilmengeWiderspruchsfreiheitLogische UhrHybridrechnerPhysikalischer EffektTupelBefehl <Informatik>ProgrammverifikationFolge <Mathematik>LeistungsbewertungAusdruck <Logik>InstantiierungNebenbedingungElement <Gruppentheorie>Spannweite <Stochastik>Strom <Mathematik>ZeitbereichAutomat <Automatentheorie>FontBildschirmfensterLogische UhrGrenzwertberechnungAlgorithmusLaufzeitfehlerMathematikSchnitt <Mathematik>Sigma-AlgebraArithmetisches MittelNeuroinformatikDatensatzSchnittmengeInstantiierungDreiecksfreier GraphMapping <Computergraphik>Spannweite <Stochastik>LeistungsbewertungProgrammschleifeAusdruck <Logik>Folge <Mathematik>WiderspruchsfreiheitProgrammverifikationBefehl <Informatik>EreignishorizontTelekommunikationProzess <Informatik>AggregatzustandPunktTeilmengeFunktionalRechter WinkelCASE <Informatik>Schiefe WahrscheinlichkeitsverteilungNebenbedingungLokales MinimumPhysikalisches SystemStellenringPhysikalischer EffektZeitzoneTupelElement <Gruppentheorie>Automat <Automatentheorie>Leistung <Physik>EntscheidungsmodellARM <Computerarchitektur>MultiplikationsoperatorKonstanteTopologieWahrscheinlichkeitsverteilungCoxeter-GruppeMereologieInterpretiererPunktwolkeMessage-PassingCOTSMAPBildschirmmaskeSprachsynthesesinc-FunktionGruppenoperationZweiComputeranimation
Globale OptimierungProzess <Informatik>MatrizenrechnungFontCASE <Informatik>LeistungsbewertungBeobachtungsstudiePhasenumwandlungSpeicherabzugParallelrechnerExtreme programmingProgrammverifikationEreignishorizontZahlenbereichParametersystemLokales MinimumBitrateMessage-PassingSchiefe WahrscheinlichkeitsverteilungPrädikat <Logik>Partielle DifferentiationSynchronisierungLaufzeitfehlerAusdruck <Logik>RechenwerkDatenbankRelationentheorieSchreiben <Datenverarbeitung>GoogolMittelwertSkalierbarkeitPunktwolkeDienst <Informatik>Mathematische LogikStetige FunktionSystemprogrammierungAusdruck <Logik>Overhead <Kommunikationstechnik>MultiplikationsoperatorEreignishorizontLaufzeitfehlerZahlenbereichTeilmengeSpannweite <Stochastik>SynchronisierungZentralisatorProzess <Informatik>t-TestMereologieARM <Computerarchitektur>sinc-FunktionRechter WinkelZweiKontrollstrukturDatenbankMatrizenrechnungAggregatzustandPhysikalisches SystemSpeicherabzugProgrammverifikationNeuroinformatikMAPGrenzschichtablösungDatenstrukturPunktCloud ComputingDatenparallelitätGemeinsamer SpeicherSelbst organisierendes SystemGlobale OptimierungInstantiierungGRASS <Programm>Projektive EbeneBillard <Mathematik>Mathematische LogikCoprozessorDickeVererbungshierarchiePunktwolkeGraphiktablettComputerarchitekturForcingLokales MinimumMessage-PassingOrdnung <Mathematik>BildschirmmaskeMathematikKnotenpunktCodierung <Programmierung>Temporale LogikSkalierbarkeitAnalytische FortsetzungParalleler AlgorithmusMultigraphSiedepunktGoogolElektronisches ForumExtreme programmingLastParametersystemLeistungsbewertungPhasenumwandlungBitrateStreaming <Kommunikationstechnik>CybersexPrädikat <Logik>NormalvektorAutomat <Automatentheorie>Schiefe WahrscheinlichkeitsverteilungLeistung <Physik>WürfelGrenzwertberechnungTopologieBefehlsprozessorMehrkernprozessorParallelrechnerOpen SourceBeobachtungsstudieCASE <Informatik>Computeranimation
AggregatzustandSimulation
Transkript: Englisch(automatisch erzeugt)