|
|
 |
|
| Journal of Information Organization | | Volume: 14, Issue: 1 ( March 2024) |
Editorial Message |
| Research |
Formal Verif ication of Systemc Using Error-Free Translation
Claude Helmstetter
Page: 1-18
Abstract_  Full_Text 2.37 MB Download: 6 times
https://doi.org/10.6025/jio/2024/14/1/1-18
Abstract: SystemC/TLMs are C++ programs that simulate embedded software before the hardware low-level description is available and are used as gold-plated models for hardware verification. Verification of SystemC/TLMs is important because a mistake in the model can deceive the system designers or reveal a defect in the specifications. There is an open-source simulator, but there are no formal verification tools. To apply model checking to System-C/TML models, you must provide semantics for standard C++ code and specific System-C/TML features. The usual approach is translating the SystemC/TML code into a formal language with a model checker. However, we suggest a different approach that eliminates the risk of error-prone translation. In the case of a system-C/TML program, transitions are obtained by running the original code using G++ and an extended systemC library. We ask the user to provide additional functions to store the current model state.These extra functions are typically less than 20% larger than the original model and allow applying all CADP verification capabilities to the SystemC/TLM model.
| Model and Instance Diagrams for Meta-modelling and Model-driven Engineering
Johan G. Granström
Page: 19-33
Abstract_ Full_Text 1.39 MB Download: 7 times
https://doi.org/10.6025/jio/2024/14/1/19-33
Abstract: Sometimes, a diagram can contain more than 1000 lines of code. Unfortunately, most software engineers abandon diagrams after the design stage and do all the actual work in code. If diagrams were code, the superiority of code over diagrams would be even greater. This paper proposes that model and instance diagrams, or equivalently class and object diagrams, become the first-level entities in a well-expressed programming language, namely type theory. The proposed semantics of diagrams are compositional and self-describing (reflexive, meta-circular). Furthermore, it is well-suited for meta-modelling and model-driven engineering, as model transformations can be proven correct in type theory. Encoding diagrams into type theory also makes them immediately useful, provided that an implementation is implemented.
| Computational Offloading for Real-Time Tasks in Embedded Systems
Anas Toma and Jian-Jia Chen
Page: 34-55
Abstract_ Full_Text 3.74 MB Download: 6 times
https://doi.org/10.6025/jio/2024/14/1/34-55
Abstract: Computation Offloading has been developed to enhance the performance of Embedded Systems by transferring the execution of specific tasks, especially computationally intensive tasks, to Servers or clouds. This paper explores computational offloading for real-time tasks in embedded systems, provided the servers guarantee response time. To decide which tasks to offload to get results in real-time, we consider frame-based real-time tasks with equivalent periods and relative deadlines. When an execution order is provided for the tasks, the problems can be solved in linear time; however, when no execution order is provided, we prove the problems to be NP-completable. To derive feasible schedules if they exist, we develop a pseudo-projective-time algorithm. We also develop an approximation scheme to trade off the algorithm’s error and complexity. We extend our algorithms to minimize the periods/ relative deadlines of the tasks for maximum performance. The algorithms are tested using a case study for a surveillance system and synthesised benchmarks.
| Notification |
AI Workshop
Monitor levels of interdisciplinary research
Open Data Report
Fourth International Conference on Digital Data Processing Yeshiva University, New York, US
5th workshop on Data For The Wellbeing of Most Vulnerable Buffalo, NY, USA
The International School on Foundations of Security Analysis and Design (FOSAD)
Book Review
|
|
|
|
|
|
|
|
Author
Rights 
