Direct Model-checking of SysML Models

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Formally verifying the correctness of software is necessary to merit the trust people put in software systems. Currently, formal verification requires human effort to prove that a piece of code matches its specification and code changes to improve verifiab ...

The potential of automatic code generation through Model-Driven Engineering (MDE) frameworks has yet to be realized. Beyond their ability to help software professionals write more accurate, reusable code, MDE frameworks could make programming accessible fo ...

Humanitarian aid-distribution programs help bring physical goods to people in need. Traditional paper-based solutions to support aid distribution do not scale to large populations and are hard to secure. Existing digital solutions solve these issues, at th ...

Code generation is an effective way to drive the complex system development in model-based systems engineering. Currently, different code generators are developed for different modeling languages to deal with the development of systems with multi-domain. T ...

Formally verifying the correctness of software network functions (NFs) is necessary for network reliability, yet existing techniques require full source code and mandate the use of specific data structures. We describe an automated technique to verify NF b ...

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...

With the continuous improvement of system scale and complexity, model-based system engineering (MBSE) is of great importance in the practice of system engineering (SE). MBSE has been widely concerned in industry, especially in the field of complex equipmen ...

Model-based systems engineering (MBSE) provides an important capability for managing the complexities of system development. MBSE empowers the formalism of system architectures for supporting model-based requirement elicitation, specification, design, deve ...

The advent of software network functions calls for stronger correctness guarantees and higher performance at every level of the stack. Current network stacks trade simplicity for performance and flexibility, especially in their driver model. We show that p ...

Software network functions (NFs), such as a network address translator, load balancer, or proxy, promise to bring flexibility and rapid innovation to computer networks and to reduce operational costs. However, continuous updates and flexibility typically c ...

Federated learning is a useful framework for centralized learning from distributed data under practical considerations of heterogeneity, asynchrony, and privacy. Federated architectures are frequently deployed in deep learning settings, which generally giv ...

Program synthesis was first proposed a few decades ago, but in the last decade it has gained increased momentum in the research community. The increasing complexity of software has dictated the urgent need for improved supporting tools that verify the soft ...

Learning to embed data into a space where similar points are together and dissimilar points are far apart is a challenging machine learning problem. In this dissertation we study two learning scenarios that arise in the context of learning embeddings and o ...

Industry is increasingly turning to reconfigurable architectures like FPGAs and CGRAs for improved performance and energy efficiency. Unfortunately, adoption of these architectures has been limited by their programming models. HDLs lack abstractions for pr ...

In this thesis, the author proposes a circular system development model which considers all the stages in a typical development process for industrial systems. In particular, the present work shows that the use of virtual prototyping at early stages of the ...

We develop approximate inference and learning methods for facilitating the use of probabilistic modeling techniques motivated by applications in two different areas. First, we consider the ill-posed inverse problem of recovering an image from an underdeter ...

Performance critical software is almost always developed in C, as programmers do not trust high-level languages to deliver the same reliable performance. This is bad because low-level code in unsafe languages attracts security vulnerabilities and because d ...

Verification is a costly task, sometimes burdensome and tedious, requiring strong formal background. To reduce the effort and cost invested in verification, we developed a model-driven approach for automatic verification of service properties, done in the ...

Modern technologies enable us to record sequences of online user activity at an unprecedented scale. Although such activity logs are abundantly available, most approaches to recommender systems are based on the rating-prediction paradigm, ignoring temporal ...

Field Programmable Gate Arrays (FPGAs) have the unique ability to be configured into application-specific architectures that are well suited to specific computing problems. This enables them to achieve performances and energy efficiencies that outclass oth ...

Direct Model-checking of SysML Models

Chat with Graph Search

Automated Formal Verification of Software Network Functions

Chat2Code: A Chatbot for Model Specification and Code Generation, The Case of Smart Contracts

Not Yet Another Digital ID: Privacy-Preserving Humanitarian Aid Distribution

Code Generation Approach Supporting Complex System Modeling based on Graph Pattern Matching

Automated Verification of Network Function Binaries

Scaling Language Features for Program Verification

Model-based Systems Engineering Papers Analysis based on Word Cloud Visualization

Design Ontology Supporting Model-Based Systems Engineering Formalisms

A Simpler and Faster NIC Driver Model for Network Functions

Verification of Software Network Functions with No Verification Expertise

Second-Order Guarantees In Federated Learning

Scaling Functional Synthesis and Repair

Learning embeddings: efficient algorithms and applications

Spatial: A Language and Compiler for Application Accelerators

Virtual Prototyping Methodology for Power Automation Cyber-Physical-Systems

Applications of Approximate Learning and Inference for Probabilistic Models

LMS-Verify: Abstraction without Regret for Verified Systems Programming’

Alignment Verification in the Early Stage of Service Design

Collaborative Recurrent Neural Networks for Dynamic Recommender Systems

FPGAs for the Masses: Affordable Hardware Synthesis from Domain-Specific Languages