Models of Control-User systems
Control-User system is a special type of parametrized systems. It is composed of a stable part (control component) and a number of dynamic components of the same type (user components). We restrict ourselves to Control-User systems in which users can communicate only with the control component and thus there is no communication between two users. Components are executing concurrently with interleaving semantics, capturing that a component can communicate with another component using the pairwise rendezvous synchronisation (a component can send a message iff the receiver is enabled).
The page contains models used in publications:
P. Varekova, B. Zimmerova, P. Moravec, and I. Cerna. Formal Verification of Systems with an Unlimited Number of Components. To appear in the IET Software journal, Volume 2, Issue 6, pages 532-546. IET Digital Library 2008. [ url | bib ]
P. Varekova and I. Cerna. Model Checking of Control-User Component-Based Parametrised Systems. In Proceedings of CBSE'08, volume 5282 of LNCS. Springer-Verlag, 2008. [ bib ]
P. Varekova and I. Cerna. Model Checking of Control-User Component-Based Parametrised Systems. Technical Report FIMU-RS-2008-06, 27 pages, Masaryk University, Faculty of Informatics, Brno, Czech Republic, July 2008. [ paper PDF | paper PS | bib ]
P. Varekova, I. Varekova, and I. Cerna. Automated Computing of the Maximal Number of Handled Clients for Client-Server Systems. In Proceedings of the Workshop on Formal Aspects of Component Software (FACS'08). To appear in ENTCS, 16 pages. 2009. [ paper | bib ]
Models of real systems:
- Cash desk and its support - specified in CoCoME, the original specification language is behavior protocols
- Subject - Observer system for 1 subject - specified in Challenge problem SAVCBS 2007, the original specification language is C-I automata
- Subject - Observer system for m subjects - specified in Challenge problem SAVCBS 2007, the original specification language is C-I automata
- Simple Subject-Observer system for 1 subject - specified in Challenge problem SAVCBS 2007, the original specification language is C-I automata
- Coordinator (Sale/CoordinatorEventHandler) system - specified in CoCoME, the original specification language is C-I automata
- Token and its support - specified as an system prototype implementation of a payment system for public Internet access on airports, the original specification language is behavior protocols
Models of simplified real systems:
- Comanche Web Server with a Multi Thread Scheduler - specified as an example application in Fractal, the original is a Java source
- Comanche Web Server with a Sequential Scheduler - specified as an example application in Fractal, the original is a Java source
Models of experimental systems:
- The controller provides 5 services in parallel - an experimental system with them minimal cutoff for 0-symmetric property 5.
- The controller provides 2 services and in all states it can receive or return any request- an experimental system.