Az informatikai rendszerek méretének növekedésével mindinkább követelmény az, hogy a rendszer nem csak funkcionalitásában legyen helyes, hanem az alkalmazott implementáció bizonyítottan helyes konstrukciót eredményezzen. Ennek egyik jellegzetes trendje a formális modellekből kiinduló automatikus kódszintézis. A rendszertervezés során a kritikus elemek vizsgálatához mindinkább formális modelleken alapuló analízist alkalmaznak a rendszertervezés fázisától kezdve. A tárgy áttekintést ad az informatikai rendszerek formális minőségi és mennyiségi modelljeinek megalkotásához és analíziséhez szükséges számításelméleti háttérről, ideértve a legfontosabb matematikai leíró paradigmákat, nyelvi realizációjukat, és a kapcsolódó analitikus és szimulációs vizsgálati módszereket. Keresztmetszeti képet ad a fenti alapismeretek alkalmazásáról az informatika területén, ideértve a rendszerszintű modellezést, a hardver tervezést, a hálózati protokollok analízisét, valamint a szoftver helyességbizonyítást.