This article reports our 7-year activity to introduce the formal method, B-Method to our college. Our activity mainly includes the mandatory short-term experiment for the whole member of the 4th-grade class (the age of 18 or 19), with few prerequisites about the logical mathematics. Under the time constraints - the course of only 140 min. per week, two or three weeks -, our experiment covers all of three fields: formal specification, proof obligation generation and model checking, and also gives the students the opportunities to briefly experience of state explosion problem. The authors set the educational goal for the experiments as giving opportunities to commit a formal method as the software engineer’s fundamental knowledge. The authors also arranged the short-time - at most 3-hour - lectures for people other than the students mentioned above who cannot write a logical predicate at all. The goal of this lecture is to give them the opportunity to find tacit facts with sound reasoning from documents. On a web page ( https://www.asahi-net.or.jp/~ny9t-oons/b-method_english.html ), the authors uploaded details - course materials, contents of models and the results of survey questions -. As far as the data of the survey questions show, it seems that the educational goal for the experiments is achieved, our experiment and lecture seem to be generally accepted, but there are some abilities to improve the methodology within the time constraint of the course.