Visible to the public Biblio

Found 1750 results

James Kollmer, Robert Irwin, Saroj Biswas,, Li Bai.  2017.  An Investigation of Cyberattacks on a Power System. 12th Intelligent Ship Symposium.

Philadelphia, PA

Qishen Zhang, Tamas Kecskes, Anastasia Mavridou, Janos Sztipanovits.  Submitted.  Towards Bridging the Gap Between Model- and Data- Driven Tool suites.

Under submission at Analytics and Mining of Model Repositories (AMMoRe)

Anastasia Mavridou, Joseph Sifakis, Janos Sztipanovits.  2017.  WebGME-BIP: A Design Studio for Modeling, Analyzing and Generating Systems with BIP.

When building large concurrent systems, one of the key difficulties lies in coordinating component behavior and, in particular, managing the access to shared resources of the execution platform. Components may interact through buses, message buffers, etc. leading to resource contention and potential deadlocks compromising safety-critical operations. The concurrent nature of such interactions is the root cause of the complexity of the resulting software. Thus, the complexity of software systems is exponential in the number of their components, making a-posteriori verification of their correctness practically infeasible. An alternative approach, taken by the BIP framework, consists in ensuring correctness-by-construction by applying automatic transformations to obtain executable code from formally defined models. Following this latter approach, we have designed and implemented a BIP design studio. We have studied extensions of the BIP language for specifying parameterized models and integrated them in the design studio to enhance scalability, reusability, and reduce model size. Additionally, we have studied and implemented a set of necessary and sufficient conditions for validating the consistency and encodability of BIP models at design time. We have developed code generation plugins from graphical BIP models to equivalent Java and BIP code. The generated BIP code can be verified for deadlock-freedom or safety properties using compositional verifications tools offered by the BIP framework.

Journal Article