Proceedings of the 7th Workshop on Models for Formal Analysis of Real Systems

Technische Samenvatting: Proceedings van de 7e Workshop over Modellen voor Formele Analyse van Realistische Systemen (MARS 2026)

Probleemstelling
Het paper identificeert twee fundamentele tekortkomingen in de huidige academische literatuur op het gebied van formele methoden en systeemmodellering:

1. Gebrek aan realisme: Veel publicaties beperken zich tot "toy examples" (speelgoedvoorbeelden) of zeer kleine casestudies. Hierdoor wordt niet aangetoond dat specificatieformalismen en modelleringstechnieken schaalbaar en toepasbaar zijn op complexe, reële systemen.
2. Ruimtebeperkingen ten koste van details: Het ontwikkelen van een accuraat model voor een reëel systeem vereist vaak maanden of jaren van werk. In traditionele papers worden echter cruciale details van deze modellen vaak weggelaten vanwege ruimtebeperkingen. De focus ligt dan uitsluitend op de formele verificatiemethodologie en de resultaten, waardoor de lessen die zijn geleerd tijdens het modelleringproces zelf verloren gaan.

Methodologie
De paper beschrijft geen nieuwe algoritmische methode, maar presenteert de proceedings (het verzamelde werk) van de 7e editie van de Workshop on Models for Formal Analysis of Real Systems (MARS 2026).

• Evenement: De workshop vond plaats op 12 april 2026 in Turijn, Italië, als satelliet-evenement van de 29e International Joint Conferences on Theory and Practice of Software (ETAPS 2026).
• Aanpak: De workshop fungeert als een platform om onderzoekers uit verschillende gemeenschappen samen te brengen die zich bezighouden met het ontwikkelen van formele modellen voor complexe systemen. De methodologische focus verschuift van puur "verificatie" naar "modellering". Het doel is om de volledige levenscyclus van het modelleren van reële systemen te documenteren, inclusief de moeilijkheden en inzichten die vaak worden genegeerd in standaardverificatiepapers.

Belangrijkste Bijdragen
De belangrijkste bijdrage van deze proceedings is het bieden van een forum en een publicatiekanaal voor gedetailleerde rapportages over:

• Grootschalige casestudies: Papers die complexe systemen behandelen in domeinen zoals netwerken, cyber-fysische systemen, hardware/software codesign en biologie.
• Modellering als einddoel: In plaats van het model slechts als een tussenstap te zien voor verificatie, worden de modellen zelf als primaire bijdrage gepresenteerd.
• Documentatie van proceskennis: Het vastleggen van de "lessen learned" (geleerde lessen) uit het modelleringsproces. Dit omvat de afwegingen die zijn gemaakt, de complexiteit die is opgelost en de details die nodig waren om een accuraat beeld van het reële systeem te krijgen.

Resultaten
Hoewel de abstract geen specifieke numerieke resultaten van individuele papers noemt, zijn de resultaten van de workshop als geheel:

• Een verzameling van papers die bewijzen dat formele specificaties toepasbaar zijn op grote, complexe reële systemen.
• Een corpus aan kennis dat de kloof dicht tussen theoretische formele methoden en de praktische implementatie in real-world scenario's.
• Het bieden van een basis voor toekomstige analyse en vergelijking van modellen, gebaseerd op gedetailleerde beschrijvingen die anders onbeschikbaar zouden zijn.

Betekenis en Impact
De significance van deze proceedings ligt in het herdefiniëren van de waarde van formele modellering in de academische gemeenschap:

• Validatie van schaalbaarheid: Het toont aan dat formele methoden niet alleen werken voor kleine voorbeelden, maar ook voor kritieke infrastructuur en complexe systemen.
• Duurzaamheid van kennis: Door de focus te leggen op het modelleringsproces in plaats van alleen op het verificatieresultaat, worden waardevolle inzichten behouden die anders verloren zouden gaan door ruimtebeperkingen in conventionele tijdschriften.
• Community-bouw: Het faciliteert de uitwisseling tussen onderzoekers uit diverse domeinen (van biologie tot hardware), wat leidt tot cross-disciplinaire innovaties in het modelleren van complexe systemen.

Kortom, deze proceedings dienen als een cruciaal referentiepunt voor onderzoekers die willen begrijpen hoe formele methoden succesvol kunnen worden toegepast op de complexiteit van de echte wereld, met een nadruk op de kwaliteit en volledigheid van het model zelf.