Formální grafický jazyk GCSR (Graphical Communicating Shared Resources) zavedený v [] slouží ke specifikaci systémů realného času. Vychází z principů Statecharts, na rozdíl od Statecharts však neklade důraz na reaktivitu. Navíc je zde speciálně zohledňováno hledisko sdílení zdrojů jednotlivými komponentami systému.
Figure: Příklad specifikace systému v grafickém formalizmu GCSR
Jak je vidět na obrázku 
(převzato z []), syntax GCSR obsahuje několik typů stavů. Speciální stavy reprezentované oválem popisují situaci, kdy systém alokuje po určitý úsek času uvedené zdroje. Například proces GD na tomto obrázku alokuje ve svém počátečním stavu zdroje cpu a gate po dobu 20 časových jednotek.
Jelikož GCSR vychází z algebry procesů ACSR (Algebra of Communicating Shared Resources) [], umožňuje abstrakci prostřednictvím operátoru restrikce akcí (Restrict) a zdrojů (Close) pro AND-stavy a OR-stavy (viz stav GU na obrázku).
Modularita je zajištěna díky kompoziční sémantice, která je definována na přechodových systémech s návěštími s relací preemptivnosti [] (řešení priorit). Syntakticky se jednotlivé moduly pojmenovávají počátečním stavem a používají pomocí stavu reprezentovaného čárkovaným obdélníkem, jak je vidět na obrázku.
Zajímavostí jsou tzv. výjimky, což jsou přechody vedoucí buď ze stavu představujícího modul nebo z AND či OR-stavu. Tyto přechody nahrazují meziúrovňové přechody známé ze Statecharts. Jsou vyvolány synchronizací s odpovídající akcí uvnitř výchozího stavu (viz akce done modulu GU na obrázku).
Systém je v GCSR dekomponován na procesy (ve smyslu algebry ACSR), které vykonávají své akce asynchronně, přičemž mohou alokovat sdílené zdroje. Akce dělíme na vstupní (značené ?) a výstupní (značené !). Každá akce má specifikovánu prioritu. Procesy spolu mohou synchronizovat pomocí párů synchronizačních akcí (vstupní a výstupní akce téhož jména). Stejně jako v CCS [] se jedná o synchronizaci vždy dvojice procesů. Komunikace v GCSR nepodporuje předávání hodnot.
V [] je formálně definována ekvivalence tohoto grafického formalizmu a algebry ACSR. To umožňuje verifikaci pomocí nástroje VERSA [], který slouží pro systémy specifikované v ACSR. Ekvivalence sémantik obou formalizmů navíc umožňuje vizualizaci výsledků verifikace v jazyce GCSR.
Grafický editor pro GCSR společně s výše uvedeným verifikačním nástrojem jsou součástí programového balíku Paragon [] pro verifikaci systémů reálného času.