Design of Cyber Bio-analytical Physical Systems: Formal methods, architectures, and multi-system interaction strategies

• Published in: Microprocessors and microsystems 2023-03, Vol.97, p.104780, Article 104780
• Main Authors: Ashraf, Kanwal, Moullec, Yannick Le, Pardy, Tamás, Rang, Toomas
• Format: Article
• Language: English
• Subjects: Biochemical analysis; Biological system modeling; Cyber Bio-analytical Physical Systems (CBPSs); Formal methods; Formal verification; Wireless networked control systems
• ISSN: 0141-9331; 1872-9436
• DOI: 10.1016/j.micpro.2023.104780

Integration of the Cyber–Physical System (CPS) concept with bio-analytical devices is highly desirable to enable device automation as well as to improve diagnostic and analytical capabilities. However, the modeling must account for entity interactions, system dynamics, and non-functional aspects required for proper device functionality. This paper presents a model-based system architecture that builds upon an extended timed automata-based formal technique. In contrast to prior works that utilized SysML or UML-based models, this allows for the wireless control of bio-analytical instruments. Using this formal method, the UPPAAL tool is used to model and test a case study called “A droplet flow cytometer for testing bacteria’s susceptibility to antibiotics”. The study shows the implications of formal techniques for the design and verification of wireless automation of high-throughput laboratory setups in Model-Based System Engineering (MBSE). Moreover, the paper extends the above aspects by adding the possibility to model multi-system interaction. This is used to analyze the trade-off between centralized and decentralized information flow strategies for better system performance under delay and bandwidth constraints. UPPAAL Stratego is used to analyze strategies for achieving specific delays and bandwidth consumption while avoiding packet losses in the event of network congestion. The results show that under strict delay constraints and high traffic, the use-case system selects the decentralized strategy over the centralized strategy. In low-traffic scenarios, the centralized strategy is more effective at ensuring the reliable operation of systems.