Research areas of the Critical Systems Research Group

The Critical Systems Research Group's (ftsrg) mission is to help engineers create reliable software systems. Our primary research area is critical software systems' design, verification, and analysis. This presentation gives an overview of the educational and R&D activities of the group, then presents recent results in the fields of blockchain, data analysis, model-based systems engineering, verification & testing, and graph-based reasoning.

Transcript

1. Overview of the research areas Zoltán Micskei, PhD research group leader https://ftsrg.mit.bme.hu/ 30th anniversary of the research group
2. 30th anniversary of the research group 2 Our research group Pataricza A. full professor Majzik I. assoc. prof. Micskei Z. assoc. prof. Gönczy L. assoc. prof. Vörös A. assoc. prof. Molnár V. asst. prof. Semeráth O. asst. prof. Huszerl G. master lecturer Varró D. full professor Klenik A. research fellow Marussy K. research fellow Farkas R. research asst. Földvári A. PhD student Elekes M. research asst. Szabó R. PhD student Szekeres D. PhD student Ficsor A. PhD student Dobos-K M. PhD student Graics B. research fellow Mondok M. PhD student Bajczi L. PhD student Nagy S. PhD student Kangogo D. PhD student N. al-Gburi PhD student Ádám Zs. PhD student Péter B. PhD student Cziborová D. PhD student N. Akel PhD student Kocsis I. assoc. prof.
3. Not just an organization unit but a team Talent care is in our DNA Targeting international standards Forging technology from science Our long-lasting values 30th anniversary of the research group 3
4. 30th anniversary of the research group 4 Education activities Elective MSc BSc Trustworthy AI and Data Analysis Systems Modeling Blockchain Technologies and Applications Data Analysis and Visualizaton for Engineers Project laboratory and thesis BSc Automated Software Engineering lab Automated Software Engineering Data Science and Artificial Intelligence major Software Engineering specialization MSc Formal Methods Software Engineering MSc Critical Systems minor Reliable Distributed and Decentralized Systems Automated Verification Techniques Critical Systems lab MSc Model-based Software Development + lab Software Engineering major
5. 30th anniversary of the research group 5 • Highly talented students – More than 150 TDK students – 50+ national prizes – Pro Scientia Gold Medal (3x) – 30+ PhD degrees • Awards for mentors – Honoris Causa Pro Scientia (highest) – Master Teacher Gold Medal (4x) – Imreh Csanád Memorial Award (2x) Talent care: students and mentors
6. Competencies & Methods DESIGN ANALYSIS VERIFICATION Automated verification Business / Mission / Safety Critical Systems Qualitative modeling Advanced tools Blockchain Data analysis Systems engineering Formal methods 30th anniversary of the research group 6
7. 30th anniversary of the research group 7 Recent and current projects Foundations Applied research Training & consultation Industrial R&D Graph Solver as a Service ADVANCE (EU RISE) AISimEval (ONR Global) DOSS (EU Horizon) EDGE-Skill (EU Digital) EU Dataspaces OpenSCALING (ITEA) SME4DD (EU Digital) Training SMEs DigitalTech (EDIH) Innovation Hub Safety Competence Center (NKFIH) Verifiable AI Technologies Model Checking as a Service Central Bank Digital Currencies (CDBC) Railway Interlocking Customized topics Blockchain, MBSE, MBT
8. 30th anniversary of the research group 8 • Blockchain: Blockchainification, Hyperledger, Projects • V&V: Safety standards, Static analysis, Testing • Modeling: MBSE, SysML, UML Training • Future technologies, methodologies • Design reviews • Test before invest Consultation • Overview of state of the art • Proof of concept demonstrators • Joint research proposals (national, EU…) R&D How to collaborate
9. Critical Systems Research Group ftsrg.mit.bme.hu ftsrg ftsrg_bme ftsrg 30th anniversary of the research group 9
10. Blockchain Application and Systems Engineering Imre Kocsis https://ftsrg.mit.bme.hu/ 30th anniversary of the research group
11. 30th anniversary of the research group • Bitcoin, Ethereum, … – Created a new system category – For/with “cryptocurrencies” – Smart contracts: “stored procedures” – No single party to trust - integrity • Emerging cross-organizational use – Bespoke, closed networks – Hyperledger Fabric – Without cryptocurrencies – Private sector: efficiency, transparency – Public sector: EBSI, MNB home ins., EMAP, … • The “middleware of trust” – From data/claim/credential validation – Through process orchestration – To “tokenization” Blockchain-based Distributed Ledger Technology 11 Multiparty consensus on “ledger” transactions By definition a critical system – needs rigorous design and extra-functional assurances
12. 30th anniversary of the research group Advancing novel applications – key activities Recent results • Hungarian Blockchain Coalition – Prof. Pataricza – member of the board – I. Kocsis: Education WG lead, L. Gönczy: FinTech WG • Supporting the EMAP project (PM/NAV) – “Eseményalapú Adatszolgáltatási Platform” pilot – Employer data provisions: event-based, single-channel – Blockchain-based implementation in preparation • CBDC research cooperation with MNB – Mapping out: blockchain  Central Bank Digital Currency – Payment, car leasing, energy support, industrial cooperation – Currently: “ecosystem” research • EDGE-Skills: data veracity in EU data spaces – Blockchain-backed Verifiable Credentials Energy price support CBDC prototype: BIS Rosalind finalist 12 Fabric  Ethereum CBDC bridge in Hyperledger Cacti Smart gas meters and readings – in production
13. 30th anniversary of the research group Systematic evaluations at design time Recent results • Performance and capacity assessment – Empirical analysis of HL Fabric performance – Exploratory Data Analysis + semantic reasoning – Component-in-the-loop evaluations – Rare event forecasting: Extreme Value Analysis • Eliminating smart contract faults – Weakness-centric treatment (not vulnerability) – Static analysis – solc-verify (Á. Hajdu@SRI) – Fault injection-based assessment of V&V – Smart-Contract-In-the-Loop model checking Impact on Fabric architecture redesign ~2017 Fabric PoCs with 1500+ TPS ftsrg: core Hyperledger member on performance 13
14. 30th anniversary of the research group MDD – for a special class of critical systems Recent results • Design exploration of architectures – Multi-aspect: Refinery graph generation + EPA – For confidentiality: Formal Concept Analysis • Generating smart contracts from models – BPMN, state charts – Zero-Knowledge Proofs for state confidentiality • Smart contract software technology – Persistence layer from domain models – Integrated static and runtime verification – Design time assurance of Fabric goodput • Emerging: Verifiable Credential engineering – ZKP-s for complex policies - e.g., energy supports – Information graph → creds: show what and whom MODELS’24 paper on architecture exploration Car leasing demonstrator in BIS Rosalind competition First steps towards systematic MDSE in support of EMAP 14
15. 30th anniversary of the research group Model-based, qualitative Error Propagation Analysis (EPA) Recent results • Mathematically sound AND practical impact reasoning – Faults → System failures; Failures → root causes; … – Classically: dependability and constraint solving – Automated fault tree and FMEA generation – a “side effect” – Static or dynamic – but qualitative • New approaches: logic reasoning-based evaluation – Answer Set Programming – Deductive/Inductive/Abductive Reasoning – Rough Set Theory for uncertainty handling • Cyber-Physical System design – IT AND OT; security AND dependability/timeliness – Qualitative reasoning for integrating the physical world • Dependability/security impact tracing: new challenges – Software Bills of Material (SBOM) – Distributed ledgers: smart contract errors Security risk assessment methodology for medium enterprises EPA for IOT in the DOSS project 15
16. Engineering Edu- cation Inno- vation 30th anniversary of the research group 16 The road ahead Education and Community - Blockchain Coalition - University courses - Hyperledger membership - SME4DD courses - Non-crypto financial applications, “unified ledgers” - Blockchain-backed Verifiable Credentials - ZKML and blockchain…? - DigitalTech EDIH - Systems Engineering: methodology - Assurances through MDD - V&V for consortial smart contracts - Runtime defenses
17. Data Analysis and Evaluation László Gönczy https://ftsrg.mit.bme.hu/ 30th anniversary of the research group
18. 30th anniversary of the research group • System models are often based on assumptions – …not on the actual data – Parameter correctness? • Data analysis not based on domain knowledge – Ad-hoc usage of methods – Interpretation of results? Actual performance? • Increasingly complex systems – Virtualization/containerization – Recently: Microservices – Correct operation under overload? – Optimized deployment? • Application and extension of – Exploratory analysis methods – Semantic/domain modelling – Lessons learned in fault tolerance Data/measurement-driven design 18
19. 30th anniversary of the research group Empirical Systems Engineering Recent results • Combining modelling and data analysis – Visual Exploratory Analysis – Ontology-based modeling and validation – Extreme Value Analysis – Logic reasoning support • Supporting multiple phases of systems engineering – High level system design and analysis – Integration of existing components – Evaluation and improvement of existing systems – Requirement conformance/compliance check – Fault injection campaigns – Benchmarking Outlier analysis/prediction in large cloud infrastructure Capacity planning and cost estimation Numerous industrial cooperations 19
20. 30th anniversary of the research group Trustworthy data-driven services Recent results • Data veracity assurance – Quality metrics+ measurement – Veracity Level Agreements – „Proof-carrying” data – Application of classical FT patterns • Emerging field: dataspaces – Decentralized (?) governance – EU + industrial initiatives – Manufacturing, energy, smart cities, skills/edu) – Data Providers + AI Services • Controlled data sharing scenarios – Robustness? – Measurement of value? – Personal data EDGE-Skills Large-scale EU pilot Ongoing: veracity assurance 20
21. 30th anniversary of the research group Process-driven design Recent results • Multiple levels of process design and analysis – „Business” processes – IT/OT operations – Data analysis/processing/ETL • Quality & effort estimation for V&V processes – Data analysis + requirement tracing – Extension of factor-based methods (CECRISMO) • Process mining – Re-design/improvement support – Conformance/compliance check – Blockchainification • Service orchestration in dataspaces – Error handling is an „increasingly important”…„ultra-complex question” – Error Propagation Analysis CECRIS: V&V cost estimation Ongoing: orchestration for data-driven services Robust data processing workflows 21
22. 30th anniversary of the research group Vision 22 • Combined logical reasoning and data analysis • Patterns for data processing and analysis • Targeted process mining methods for re-engineering Research • Data veracity assurance in different domains • (Semi-) automated EDA • Impact analysis and evaluation Engineering • Empirical Systems Engineering (PhD) • Trustworthy AI and Data Analysis (MSc) • Data analysis and visualization for engineers • EDIH courses/consultations Education
23. Model-Based Systems Engineering Vince Molnár https://ftsrg.mit.bme.hu/ 30th anniversary of the research group
24. 30th anniversary of the research group Systems Engineering • Rigorous design of complex systems Model-Based Systems Engineering • Represent information in models • Model = Structured data = Machine assistance • Increasing popularity in critical domains – Automotive, Aviation, Space, Railway, etc. • Revolutionary emerging standards • International collaborative efforts Model-Based Systems Engineering – Now 24
25. 30th anniversary of the research group Model-Based Systems Engineering Recent results Methodology • Platform-based MBSE for HW-SW co-design • V&V and Analysis integrations Language • UML, SysML and SysML v2 • Domain-specific languages Flexible and customizable training and consultation Customized MBSE methodologies for automotive industry OpenSCALING project to integrate MBSE with simulation Journal papers about language semantics and standards 25
26. 30th anniversary of the research group Next-Generation MBSE – SysML v2 Recent results Participation • Authorship in the specification • SMC Leadership • Formal Methods WG (leading) • Conformance WG (leading) • Execution WG (core member) • Semantics WG (core member) • Reference Implementation WG • Certification WG Several new partners and cooperations First SysML v2 formal verification and model generator tool Coordinating first academic paper about SysML v2 verification 26
27. 30th anniversary of the research group Automated V&V in Systems Engineering Recent results “Use your models!” • Semantic analysis • Early verification of critical requirements • Code/Test/Monitor generation Gamma: Bridge MBSE and FM • Formal verification integrated into SysML, SysML v2 and DSLs Several conference and journal papers since Majzik et al. Automated analysis and generation for railway systems Automated formal methods in engineering workflows (NASA, IQL) 27
28. 30th anniversary of the research group Our Vision: Automated MBSE Assistance 28 Flexible and efficient MBSE throughout the whole lifecycle Early analysis and efficient verification Dynamic prototyping Methodology Language Tool support Smart assistance Generative modeling Model validation Semantic analysis Tool integrations Formal verification Dynamic exploration Executable models Code generation Test generation Monitor generation *-in-the-loop
29. Verification and Testing András Vörös https://ftsrg.mit.bme.hu/ 30th anniversary of the research group
30. 30th anniversary of the research group • Will my system operate correctly? – Verification of functional correctness and ensure extra-functional properties – Find design/implementation errors • What can we use? – Simulation, testing, formal verification • Impact of our work: – Improved product quality – New, more efficient and expressive verification algorithms and methodologies (System) Analysis to Ensure Correctness 30 Source: pexels.com
31. 30th anniversary of the research group Systems Engineering for Safety • Design support for fault- tolerant critical systems – Engineering language extensions – Rapid evaluation of design variants/prototypes – Finding weak points in design – Sensitivity/Causation analysis • Efficient analysis algorithms – Simulation-based methods using deep-learning for rapid evaluation – Numerical methods for accuracy 31 Recent results Applications in the automotive, railway and energy domain Several papers in dependability related conferences Integrated engineering toolchain for performability analysis
32. 30th anniversary of the research group Finding Critical Design Errors (Testing) • Automatic test generation – Using design/domain models – Ensure coverage – Focus on critical behavior • Test generation integrated to design tools – Distributed/critical systems • Beyond traditional areas – AI/Autonomous/ADAS – Domain specific languages – SysML v2 language 32 Recent results Model-based test generation for an industrial use-case Testing of an ADAS AI-based lane keeping component Several conference and journal papers (TSE, MODELS) OpenPilot Lane keeping
33. 30th anniversary of the research group Finding Critical Design Errors (Verification) • Methodology to find errors in system design • State-of-the-art verification algorithms – (Concurrent) software verification – Real-time systems – High-level engineering models – Component-based systems 33 Recent results Found real problems in industrial use-cases (automotive, railway) Recent theta awards: Distinguished artifact Horn close competition Last 5 years: 17 first prizes in university level TDK competitions
34. 30th anniversary of the research group 34 • Strong background in algorithm development • Scale up to industrial problems – Open-source tool development • Extend the approaches to new application areas – AI verification/testing – Blockchain – SysML v2 Vision New analysis algorithms for correctness verification Industrial adaptation New applications and areas
35. Model Transformation and Generation Oszkár Semeráth https://ftsrg.mit.bme.hu/ 30th anniversary of the research group
36. 30th anniversary of the research group • Context: graph are widely used in knowledge representation and analysis • Scenarios: testing, benchmarking, or generative architecture rely on graphs • Approach: graph analysis + generation (consistent|realistic|diverse|scalable) • Precise algorithms • Powerful tools Graph-based reasoning 36 System models Database content Test environments github.com/BerkeleyLearnVerify/Scenic Data Structures Sagiv, M., Reps, T., & Wilhelm, R. (2002). Parametric shape analysis via 3-valued logic. x,r y,r e,r n n x,r y,r e,r n n e,r n n →
37. v1 v2 v3 30th anniversary of the research group Graph analysis and synthesis • Powerful mathematical analysis techniques for models • Novel graph-based logic solver for the automated synthesis of design alternatives • Precision + Scalability • Goal: solve problems with complex structure 37   validation $$$ cost  performance %% coverage synthesis transition Transition state2 State target sct Statechart region egion reg ons region2 egion reg ons state State er es entry2 Entry er es nalState FinalState er es choice Choice er es entry Entry er es er es transition2 Transition ou go ng r ns on transition Transition ou go ng r ns on transition Transition ou go ng r ns on target transition4 Transition ou go ng r ns on target ou go ng r ns on transition Transition ou go ng r ns on target target target analysis Recent Results • Top papers ICSE, TSE - No accepted paper from Hungarian authors in decades • Research project VERIFIABLE AI/ML TECHNIQUES FOR PNT APPLICATIONS
38. 30th anniversary of the research group Modern tools • We are experts in tool development • Interactive state-of-the-art web-based editors • Generation algorithms running on server • Various domains blockchain architecture|chemical reaction railway topology|modeling environment, satellite network|video game maps • Goal: support engineers and experts solving problems 38 Recent Results • Refinery Continuously deployed: https://refinery.tools • Amazon Research Award First in the region
39. 30th anniversary of the research group Verification/Testing of AI/ML Applications • AI applications are data-oriented systems • Complex, dynamic environment • Novel generation + Advanced simulators → Diverse tests • Systematic testing of AI applications 39 front left visible visible Recent Results • R&D project with railway company • Research project with USA Navy Office of Naval Research Global
40. consistency guarantees complex structure challenging domains 30th anniversary of the research group Vision: Neuro-Symbolic Reasoning 40 logic reasoning graph transformation neural networks